141 xml_of_proof prf :: |
141 xml_of_proof prf :: |
142 (case optt of NONE => [] | SOME t => [xml_of_term t])) |
142 (case optt of NONE => [] | SOME t => [xml_of_term t])) |
143 | xml_of_proof (prf %% prf') = |
143 | xml_of_proof (prf %% prf') = |
144 XML.Elem ("AppP", [], [xml_of_proof prf, xml_of_proof prf']) |
144 XML.Elem ("AppP", [], [xml_of_proof prf, xml_of_proof prf']) |
145 | xml_of_proof (Hyp t) = XML.Elem ("Hyp", [], [xml_of_term t]) |
145 | xml_of_proof (Hyp t) = XML.Elem ("Hyp", [], [xml_of_term t]) |
146 | xml_of_proof (PThm ((s, _), _, t, optTs)) = |
146 | xml_of_proof (PThm (s, _, t, optTs)) = |
147 XML.Elem ("PThm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs) |
147 XML.Elem ("PThm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs) |
148 | xml_of_proof (PAxm (s, t, optTs)) = |
148 | xml_of_proof (PAxm (s, t, optTs)) = |
149 XML.Elem ("PAxm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs) |
149 XML.Elem ("PAxm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs) |
150 | xml_of_proof (Oracle (s, t, optTs)) = |
150 | xml_of_proof (Oracle (s, t, optTs)) = |
151 XML.Elem ("Oracle", [("name", s)], xml_of_term t :: xml_of_opttypes optTs) |
151 XML.Elem ("Oracle", [("name", s)], xml_of_term t :: xml_of_opttypes optTs) |