1 (* simplification of terms
2 author: Walther Neuper 050912
3 (c) due to copyright terms
5 use"Knowledge/Simplify.ML";
10 (** interface isabelle -- isac **)
12 theory' := overwritel (!theory', [("Simplify.thy",Simplify.thy)]);
17 (prep_pbt Simplify.thy "pbl_simp" [] e_pblID
19 [("#Given" ,["term t_"]),
20 ("#Find" ,["normalform n_"])
22 append_rls "e_rls" e_rls [(*for preds in where_*)],
27 (prep_pbt Simplify.thy "pbl_vereinfache" [] e_pblID
29 [("#Given" ,["term t_"]),
30 ("#Find" ,["normalform n_"])
32 append_rls "e_rls" e_rls [(*for preds in where_*)],
33 SOME "Vereinfache t_",
39 (prep_met Simplify.thy "met_simp" [] e_metID
41 [("#Given" ,["term t_"]),
42 ("#Find" ,["normalform n_"])
44 {rew_ord'="tless_true",
49 crls = e_rls, nrls = e_rls},
55 (*.function for handling the cas-input "Simplify (2*a + 3*a)":
56 make a model which is already in ptree-internal format.*)
57 (* val (h,argl) = strip_comb (str2term "Simplify (2*a + 3*a)");
58 val (h,argl) = strip_comb ((term_of o the o (parse thy))
59 "Simplify (2*a + 3*a)");
62 [((term_of o the o (parse thy)) "term", t),
63 ((term_of o the o (parse thy)) "normalform",
64 [(term_of o the o (parse thy)) "N"])
66 | argl2dtss _ = raise error "Simplify.ML: wrong argument for argl2dtss";
70 [((term_of o the o (parse thy)) "Simplify",
71 (("Isac.thy", ["simplification"], ["no_met"]),
73 ((term_of o the o (parse thy)) "Vereinfache",
74 (("Isac.thy", ["vereinfachen"], ["no_met"]),