equal
deleted
inserted
replaced
35 |
35 |
36 "----------- parsing ---------------------------------------------"; |
36 "----------- parsing ---------------------------------------------"; |
37 "----------- parsing ---------------------------------------------"; |
37 "----------- parsing ---------------------------------------------"; |
38 "----------- parsing ---------------------------------------------"; |
38 "----------- parsing ---------------------------------------------"; |
39 fun str2term str = (term_of o the o (parse Integrate.thy)) str; |
39 fun str2term str = (term_of o the o (parse Integrate.thy)) str; |
40 fun term2s t = Sign.string_of_term (sign_of Integrate.thy) t; |
40 fun term2s t = Syntax.string_of_term (thy2ctxt' "Integrate") t; |
41 |
41 |
42 val t = str2term "Integral x D x"; |
42 val t = str2term "Integral x D x"; |
43 val t = str2term "Integral x^^^2 D x"; |
43 val t = str2term "Integral x^^^2 D x"; |
44 atomty t; |
44 atomty t; |
45 |
45 |