equal
deleted
inserted
replaced
27 |
27 |
28 ML {* |
28 ML {* |
29 |
29 |
30 (** problems **) |
30 (** problems **) |
31 store_pbt |
31 store_pbt |
32 (prep_pbt Simplify.thy "pbl_simp" [] e_pblID |
32 (prep_pbt (theory "Simplify") "pbl_simp" [] e_pblID |
33 (["simplification"], |
33 (["simplification"], |
34 [("#Given" ,["term t_"]), |
34 [("#Given" ,["term t_"]), |
35 ("#Find" ,["normalform n_"]) |
35 ("#Find" ,["normalform n_"]) |
36 ], |
36 ], |
37 append_rls "e_rls" e_rls [(*for preds in where_*)], |
37 append_rls "e_rls" e_rls [(*for preds in where_*)], |
38 SOME "Simplify t_", |
38 SOME "Simplify t_", |
39 [])); |
39 [])); |
40 |
40 |
41 store_pbt |
41 store_pbt |
42 (prep_pbt Simplify.thy "pbl_vereinfache" [] e_pblID |
42 (prep_pbt (theory "Simplify") "pbl_vereinfache" [] e_pblID |
43 (["vereinfachen"], |
43 (["vereinfachen"], |
44 [("#Given" ,["term t_"]), |
44 [("#Given" ,["term t_"]), |
45 ("#Find" ,["normalform n_"]) |
45 ("#Find" ,["normalform n_"]) |
46 ], |
46 ], |
47 append_rls "e_rls" e_rls [(*for preds in where_*)], |
47 append_rls "e_rls" e_rls [(*for preds in where_*)], |
49 [])); |
49 [])); |
50 |
50 |
51 (** methods **) |
51 (** methods **) |
52 |
52 |
53 store_met |
53 store_met |
54 (prep_met Simplify.thy "met_simp" [] e_metID |
54 (prep_met (theory "Simplify") "met_simp" [] e_metID |
55 (["simplification"], |
55 (["simplification"], |
56 [("#Given" ,["term t_"]), |
56 [("#Given" ,["term t_"]), |
57 ("#Find" ,["normalform n_"]) |
57 ("#Find" ,["normalform n_"]) |
58 ], |
58 ], |
59 {rew_ord'="tless_true", |
59 {rew_ord'="tless_true", |