255 XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Method")]), [xml_of_strs ct]) |
255 XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Method")]), [xml_of_strs ct]) |
256 | xml_of_tac (Tactic.Specify_Problem ct) = |
256 | xml_of_tac (Tactic.Specify_Problem ct) = |
257 XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Problem")]), [xml_of_strs ct]) |
257 XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Problem")]), [xml_of_strs ct]) |
258 | xml_of_tac tac = raise ERROR ("xml_of_tac: not impl. for " ^ Tactic.input_to_string tac); |
258 | xml_of_tac tac = raise ERROR ("xml_of_tac: not impl. for " ^ Tactic.input_to_string tac); |
259 |
259 |
260 val e_pblterm = (Thm.term_of o the o (TermC.parse @{theory Prog_Tac})) |
260 val e_pblterm = TermC.parseNEW'' @{theory Prog_Tac} |
261 ("Problem (" ^ ThyC.id_empty ^ ", " ^ strs2str' Problem.id_empty ^ ")"); |
261 ("Problem (" ^ ThyC.id_empty ^ ", " ^ strs2str' Problem.id_empty ^ ")"); |
262 |
262 |
263 (*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*) |
263 (*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*) |
264 fun xml_of_posterm (p, t, _) = |
264 fun xml_of_posterm (p, t, _) = |
265 let val input_request = Free ("________________________________________________", dummyT) |
265 let val input_request = Free ("________________________________________________", dummyT) |