equal
deleted
inserted
replaced
39 val preconds2xml : int -> (bool * Term.term) list -> Celem.xml |
39 val preconds2xml : int -> (bool * Term.term) list -> Celem.xml |
40 val rls2xml : int -> ThyC.id * Rule_Set.T -> Celem.xml |
40 val rls2xml : int -> ThyC.id * Rule_Set.T -> Celem.xml |
41 val rule2xml : int -> Check_Unique.guh -> Rule.rule -> Celem.xml |
41 val rule2xml : int -> Check_Unique.guh -> Rule.rule -> Celem.xml |
42 val rules2xml : int -> Check_Unique.guh -> Rule.rule list -> Celem.xml |
42 val rules2xml : int -> Check_Unique.guh -> Rule.rule list -> Celem.xml |
43 val scr2xml : int -> Program.T -> Celem.xml |
43 val scr2xml : int -> Program.T -> Celem.xml |
44 val spec2xml : int -> Spec.spec -> Celem.xml |
44 val spec2xml : int -> Spec.T -> Celem.xml |
45 val sub2xml : int -> Term.term * Term.term -> Celem.xml |
45 val sub2xml : int -> Term.term * Term.term -> Celem.xml |
46 val subs2xml : int -> Selem.subs -> Celem.xml |
46 val subs2xml : int -> Selem.subs -> Celem.xml |
47 val subst2xml : int -> UnparseC.subst -> Celem.xml |
47 val subst2xml : int -> UnparseC.subst -> Celem.xml |
48 val tac2xml : int -> Tactic.input -> Celem.xml |
48 val tac2xml : int -> Tactic.input -> Celem.xml |
49 val tacs2xml : int -> Tactic.input list -> Celem.xml |
49 val tacs2xml : int -> Tactic.input list -> Celem.xml |
639 (XML.Elem (("STRINGLISTTACTIC", [ |
639 (XML.Elem (("STRINGLISTTACTIC", [ |
640 ("name", "Specify_Problem")]), [ct])) = Tactic.Specify_Problem (xml_to_strs ct) |
640 ("name", "Specify_Problem")]), [ct])) = Tactic.Specify_Problem (xml_to_strs ct) |
641 | xml_to_tac x = raise ERROR ("xml_to_tac: not impl. for " ^ xmlstr 0 x); |
641 | xml_to_tac x = raise ERROR ("xml_to_tac: not impl. for " ^ xmlstr 0 x); |
642 |
642 |
643 val e_pblterm = (Thm.term_of o the o (TermC.parse @{theory Prog_Tac})) |
643 val e_pblterm = (Thm.term_of o the o (TermC.parse @{theory Prog_Tac})) |
644 ("Problem (" ^ ThyC.id_empty ^ "," ^ strs2str' Spec.e_pblID ^ ")"); |
644 ("Problem (" ^ ThyC.id_empty ^ "," ^ strs2str' Problem.id_empty ^ ")"); |
645 |
645 |
646 (*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*) |
646 (*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*) |
647 fun xml_of_posterm (p, t, _) = |
647 fun xml_of_posterm (p, t, _) = |
648 let val input_request = Free ("________________________________________________", dummyT) |
648 let val input_request = Free ("________________________________________________", dummyT) |
649 in |
649 in |