183 rew_ord = ("termlessI",termlessI), |
183 rew_ord = ("termlessI",termlessI), |
184 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls |
184 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls |
185 [(*for asm in NTH_CONS ...*) |
185 [(*for asm in NTH_CONS ...*) |
186 Calc ("op <",eval_equ "#less_"), |
186 Calc ("op <",eval_equ "#less_"), |
187 (*2nd NTH_CONS pushes n+-1 into asms*) |
187 (*2nd NTH_CONS pushes n+-1 into asms*) |
188 Calc("op +", eval_binop "#add_") |
188 Calc("Groups.plus_class.plus", eval_binop "#add_") |
189 ], |
189 ], |
190 srls = Erls, calc = [], |
190 srls = Erls, calc = [], |
191 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}), |
191 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}), |
192 Calc("op +", eval_binop "#add_"), |
192 Calc("Groups.plus_class.plus", eval_binop "#add_"), |
193 Thm ("NTH_NIL",num_str @{thm NTH_NIL}), |
193 Thm ("NTH_NIL",num_str @{thm NTH_NIL}), |
194 Calc("Tools.lhs", eval_lhs"eval_lhs_"), |
194 Calc("Tools.lhs", eval_lhs"eval_lhs_"), |
195 Calc("Tools.rhs", eval_rhs"eval_rhs_"), |
195 Calc("Tools.rhs", eval_rhs"eval_rhs_"), |
196 Calc("Atools.argument'_in", |
196 Calc("Atools.argument'_in", |
197 eval_argument_in "Atools.argument'_in") |
197 eval_argument_in "Atools.argument'_in") |
204 rew_ord = ("termlessI",termlessI), |
204 rew_ord = ("termlessI",termlessI), |
205 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls |
205 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls |
206 [(*for asm in NTH_CONS ...*) |
206 [(*for asm in NTH_CONS ...*) |
207 Calc ("op <",eval_equ "#less_"), |
207 Calc ("op <",eval_equ "#less_"), |
208 (*2nd NTH_CONS pushes n+-1 into asms*) |
208 (*2nd NTH_CONS pushes n+-1 into asms*) |
209 Calc("op +", eval_binop "#add_") |
209 Calc("Groups.plus_class.plus", eval_binop "#add_") |
210 ], |
210 ], |
211 srls = Erls, calc = [], |
211 srls = Erls, calc = [], |
212 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}), |
212 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}), |
213 Calc("op +", eval_binop "#add_"), |
213 Calc("Groups.plus_class.plus", eval_binop "#add_"), |
214 Thm ("NTH_NIL", num_str @{thm NTH_NIL}), |
214 Thm ("NTH_NIL", num_str @{thm NTH_NIL}), |
215 Calc("Tools.lhs", eval_lhs "eval_lhs_"), |
215 Calc("Tools.lhs", eval_lhs "eval_lhs_"), |
216 Calc("Atools.filter'_sameFunId", |
216 Calc("Atools.filter'_sameFunId", |
217 eval_filter_sameFunId "Atools.filter'_sameFunId"), |
217 eval_filter_sameFunId "Atools.filter'_sameFunId"), |
218 (*WN070514 just for smltest/../biegelinie.sml ...*) |
218 (*WN070514 just for smltest/../biegelinie.sml ...*) |