equal
deleted
inserted
replaced
68 [((Thm.term_of o the o (TermC.parse thy)) "Simplify", |
68 [((Thm.term_of o the o (TermC.parse thy)) "Simplify", |
69 (("Isac_Knowledge", ["simplification"], ["no_met"]), argl2dtss)), |
69 (("Isac_Knowledge", ["simplification"], ["no_met"]), argl2dtss)), |
70 ((Thm.term_of o the o (TermC.parse thy)) "Vereinfache", |
70 ((Thm.term_of o the o (TermC.parse thy)) "Vereinfache", |
71 (("Isac_Knowledge", ["vereinfachen"], ["no_met"]), argl2dtss))]\<close> |
71 (("Isac_Knowledge", ["vereinfachen"], ["no_met"]), argl2dtss))]\<close> |
72 |
72 |
|
73 ML \<open> |
|
74 \<close> ML \<open> |
|
75 \<close> ML \<open> |
|
76 \<close> |
73 end |
77 end |