equal
deleted
inserted
replaced
157 fun xml_of_subs (subs : Subst.input) = |
157 fun xml_of_subs (subs : Subst.input) = |
158 XML.Elem (("SUBSTITUTION", []), |
158 XML.Elem (("SUBSTITUTION", []), |
159 map xml_of_sub (Tactic.subst_adapt_to_type (ThyC.id_to_ctxt "Isac_Knowledge") subs)) |
159 map xml_of_sub (Tactic.subst_adapt_to_type (ThyC.id_to_ctxt "Isac_Knowledge") subs)) |
160 fun xml_of_sube sube = |
160 fun xml_of_sube sube = |
161 XML.Elem (("SUBSTITUTION", []), |
161 XML.Elem (("SUBSTITUTION", []), |
162 map xml_of_sub (Subst.T_from_string_eqs (ThyC.get_theory "Isac_Knowledge") sube)) |
162 map xml_of_sub (Subst.T_from_string_eqs (Know_Store.get_via_last_thy "Isac_Knowledge") sube)) |
163 |
163 |
164 fun thm''2xml j (thm : thm) = |
164 fun thm''2xml j (thm : thm) = |
165 indt j ^ "<THEOREM>\n" ^ |
165 indt j ^ "<THEOREM>\n" ^ |
166 indt (j+i) ^ "<ID> " ^ ThmC.id_of_thm thm ^ " </ID>\n"^ |
166 indt (j+i) ^ "<ID> " ^ ThmC.id_of_thm thm ^ " </ID>\n"^ |
167 term2xml j (Thm.prop_of thm) ^ "\n" ^ |
167 term2xml j (Thm.prop_of thm) ^ "\n" ^ |