equal
deleted
inserted
replaced
71 fun argl2dtss t = |
71 fun argl2dtss t = |
72 [((term_of o the o (parse thy)) "TERM", t), |
72 [((term_of o the o (parse thy)) "TERM", t), |
73 ((term_of o the o (parse thy)) "normalform", |
73 ((term_of o the o (parse thy)) "normalform", |
74 [(term_of o the o (parse thy)) "N"]) |
74 [(term_of o the o (parse thy)) "N"]) |
75 ] |
75 ] |
76 | argl2dtss _ = raise error "Simplify.ML: wrong argument for argl2dtss"; |
76 | argl2dtss _ = error "Simplify.ML: wrong argument for argl2dtss"; |
77 |
77 |
78 castab := |
78 castab := |
79 overwritel (!castab, |
79 overwritel (!castab, |
80 [((term_of o the o (parse thy)) "Simplify", |
80 [((term_of o the o (parse thy)) "Simplify", |
81 (("Isac", ["simplification"], ["no_met"]), |
81 (("Isac", ["simplification"], ["no_met"]), |