equal
deleted
inserted
replaced
65 (*WN071016 checked that _all_ Frontend/interface.sml uses this*) |
65 (*WN071016 checked that _all_ Frontend/interface.sml uses this*) |
66 fun term2xml j t = |
66 fun term2xml j t = |
67 indt (j+i) ^ "<MATHML>\n" ^ |
67 indt (j+i) ^ "<MATHML>\n" ^ |
68 indt (j+2*i) ^ "<ISA> " ^ (decode o UnparseC.term) t ^ " </ISA>\n" ^ |
68 indt (j+2*i) ^ "<ISA> " ^ (decode o UnparseC.term) t ^ " </ISA>\n" ^ |
69 indt (j+i) ^ "</MATHML>"; |
69 indt (j+i) ^ "</MATHML>"; |
70 (*val t = str2term "equality e_"; |
70 (*val t = TermC.parse_test @{context} "equality e_"; |
71 writeln (term2xml 8 t); |
71 writeln (term2xml 8 t); |
72 <MATHML> |
72 <MATHML> |
73 <ISA> equality e_ </ISA> |
73 <ISA> equality e_ </ISA> |
74 <MATHML> *) |
74 <MATHML> *) |
75 fun xml_of_term t = |
75 fun xml_of_term t = |