Hi Bill
2013/5/4 Bill Richter
> Question: given the string of a theorem "IN_ELIM_THM", how can I access
> the theorem IN_ELIM_THM? Or given a string of a thm_list->tactic
> "MESON_TAC", how can I access MESON_TAC?
# let get = Obj.magic o Toploop.getvalue;;
val get : string -> 'a =
# ((get "I
Question: given the string of a theorem "IN_ELIM_THM", how can I access the
theorem IN_ELIM_THM? Or given a string of a thm_list->tactic "MESON_TAC", how
can I access MESON_TAC? This is a problem that Freek must have solved in
miz3.ml, but I can't figure out how. John did not seem to solve it
