33 |
33 |
34 ML \<open> |
34 ML \<open> |
35 val thy = @{theory}; |
35 val thy = @{theory}; |
36 |
36 |
37 val eval_rls = prep_rls' ( |
37 val eval_rls = prep_rls' ( |
38 Rule_Set.Rls {id = "eval_rls", preconds = [], rew_ord = ("termlessI", termlessI), |
38 Rule_Def.Repeat {id = "eval_rls", preconds = [], rew_ord = ("termlessI", termlessI), |
39 erls = Rule_Set.e_rls, srls = Rule_Set.Erls, calc = [], errpatts = [], |
39 erls = Rule_Set.e_rls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
40 rules = [Rule.Thm ("refl", TermC.num_str @{thm refl}), |
40 rules = [Rule.Thm ("refl", TermC.num_str @{thm refl}), |
41 Rule.Thm ("order_refl", TermC.num_str @{thm order_refl}), |
41 Rule.Thm ("order_refl", TermC.num_str @{thm order_refl}), |
42 Rule.Thm ("radd_left_cancel_le", TermC.num_str @{thm radd_left_cancel_le}), |
42 Rule.Thm ("radd_left_cancel_le", TermC.num_str @{thm radd_left_cancel_le}), |
43 Rule.Thm ("not_true", TermC.num_str @{thm not_true}), |
43 Rule.Thm ("not_true", TermC.num_str @{thm not_true}), |
44 Rule.Thm ("not_false", TermC.num_str @{thm not_false}), |
44 Rule.Thm ("not_false", TermC.num_str @{thm not_false}), |