equal
deleted
inserted
replaced
712 in assbl_thm deriv thy_ref tags maxidx shyps hyps tpairs prop' end; |
712 in assbl_thm deriv thy_ref tags maxidx shyps hyps tpairs prop' end; |
713 |
713 |
714 fun get_thm' xstring = (*?covers 2009 Thm?!, replaces 2002 fun get_thm : |
714 fun get_thm' xstring = (*?covers 2009 Thm?!, replaces 2002 fun get_thm : |
715 val it = fn : Theory.theory -> xstring -> Thm.thm*) |
715 val it = fn : Theory.theory -> xstring -> Thm.thm*) |
716 Thm (xstring, |
716 Thm (xstring, |
717 num_str (ProofContext.get_thm (ctxt_Isac"") xstring)); |
717 num_str (ProofContext.get_thm (thy2ctxt' "Isac") xstring)); |
718 |
718 |
719 (** get types of Free and Abs for parse' **) |
719 (** get types of Free and Abs for parse' **) |
720 (*11.1.00: not used, fix-typed +,*,-,^ instead *) |
720 (*11.1.00: not used, fix-typed +,*,-,^ instead *) |
721 |
721 |
722 val dummyT = Type ("dummy",[]); |
722 val dummyT = Type ("dummy",[]); |