144 |
144 |
145 ML{* (*the former ListC.ML*) |
145 ML{* (*the former ListC.ML*) |
146 (** rule set for evaluating listexpr in scripts **) |
146 (** rule set for evaluating listexpr in scripts **) |
147 val list_rls = |
147 val list_rls = |
148 Rls{id="list_rls",preconds = [], rew_ord = ("dummy_ord",dummy_ord), |
148 Rls{id="list_rls",preconds = [], rew_ord = ("dummy_ord",dummy_ord), |
149 erls = e_rls, srls = Erls, calc = [], errpatts = [], |
149 erls = Erls, srls = Erls, calc = [], errpatts = [], |
150 rules = (*8.01: copied from*) |
150 rules = (*8.01: copied from*) |
151 [Thm ("refl", num_str @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*) |
151 [Thm ("refl", num_str @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*) |
152 Thm ("o_apply", num_str @{thm o_apply}), |
152 Thm ("o_apply", num_str @{thm o_apply}), |
153 |
153 |
154 Thm ("NTH_CONS",num_str @{thm NTH_CONS}),(*erls for cond. in Atools.ML*) |
154 Thm ("NTH_CONS",num_str @{thm NTH_CONS}),(*erls for cond. in Atools.ML*) |