equal
deleted
inserted
replaced
129 |
129 |
130 subsection \<open>rule set for evaluating Porg_Expr, will be extended in several thys\<close> |
130 subsection \<open>rule set for evaluating Porg_Expr, will be extended in several thys\<close> |
131 ML \<open> |
131 ML \<open> |
132 \<close> ML \<open> |
132 \<close> ML \<open> |
133 val prog_expr = |
133 val prog_expr = |
134 Rule_Def.Repeat {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
134 Rule_Def.Repeat {id = "prog_expr", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
135 erls = Rule_Def.Empty, srls = Rule_Def.Empty, calc = [], errpatts = [], |
135 erls = Rule_Def.Empty, srls = Rule_Def.Empty, calc = [], errpatts = [], |
136 rules = [Rule_Def.Thm ("refl", @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*) |
136 rules = [Rule_Def.Thm ("refl", @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*) |
137 Rule_Def.Thm ("o_apply", @{thm o_apply}), |
137 Rule_Def.Thm ("o_apply", @{thm o_apply}), |
138 |
138 |
139 Rule_Def.Thm ("NTH_CONS", @{thm NTH_CONS}),(*erls for cond. in Atools.ML*) |
139 Rule_Def.Thm ("NTH_CONS", @{thm NTH_CONS}),(*erls for cond. in Atools.ML*) |