32 [("#Given", ["Term t_t"]), |
32 [("#Given", ["Term t_t"]), |
33 ("#Find", ["normalform n_n"])], |
33 ("#Find", ["normalform n_n"])], |
34 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "Vereinfache t_t", []))]\<close> |
34 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "Vereinfache t_t", []))]\<close> |
35 |
35 |
36 (** methods **) |
36 (** methods **) |
37 setup \<open>KEStore_Elems.add_mets |
37 |
38 [MethodC.prep_input @{theory} "met_tsimp" [] MethodC.id_empty |
38 method met_tsimp : "simplification" = |
39 (["simplification"], |
39 \<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Rule_Set.empty, |
40 [("#Given" ,["Term t_t"]), |
40 errpats = [], nrls = Rule_Set.empty}\<close> |
41 ("#Find" ,["normalform n_n"])], |
41 Given: "Term t_t" |
42 {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Rule_Set.empty, |
42 Find: "normalform n_n" |
43 errpats = [], nrls = Rule_Set.empty}, |
|
44 @{thm refl})] |
|
45 \<close> |
|
46 |
43 |
47 ML \<open> |
44 ML \<open> |
48 |
45 |
49 (** CAS-command **) |
46 (** CAS-command **) |
50 |
47 |