152 proof_of_xml proof % NONE |
152 proof_of_xml proof % NONE |
153 | proof_of_xml (XML.Elem ("Appt", [], [proof, term])) = |
153 | proof_of_xml (XML.Elem ("Appt", [], [proof, term])) = |
154 proof_of_xml proof % SOME (term_of_xml term) |
154 proof_of_xml proof % SOME (term_of_xml term) |
155 | proof_of_xml (XML.Elem ("AppP", [], [proof, proof'])) = |
155 | proof_of_xml (XML.Elem ("AppP", [], [proof, proof'])) = |
156 proof_of_xml proof %% proof_of_xml proof' |
156 proof_of_xml proof %% proof_of_xml proof' |
|
157 | proof_of_xml (XML.Elem ("Hyp", [], [term])) = |
|
158 Hyp (term_of_xml term) |
157 | proof_of_xml (XML.Elem ("PThm", [("name", s)], term :: opttypes)) = |
159 | proof_of_xml (XML.Elem ("PThm", [("name", s)], term :: opttypes)) = |
158 PThm (s, MinProof ([], [], []), (* FIXME? *) |
160 PThm (s, MinProof ([], [], []), (* FIXME? *) |
159 term_of_xml term, opttypes_of_xml opttypes) |
161 term_of_xml term, opttypes_of_xml opttypes) |
160 | proof_of_xml (XML.Elem ("PAxm", [("name", s)], term :: opttypes)) = |
162 | proof_of_xml (XML.Elem ("PAxm", [("name", s)], term :: opttypes)) = |
161 PAxm (s, term_of_xml term, opttypes_of_xml opttypes) |
163 PAxm (s, term_of_xml term, opttypes_of_xml opttypes) |