equal
deleted
inserted
replaced
181 val srls = Rls {id="srls_IntegrierenUnd..", |
181 val srls = Rls {id="srls_IntegrierenUnd..", |
182 preconds = [], |
182 preconds = [], |
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 ("Orderings.ord_class.less",eval_equ "#less_"), |
187 (*2nd NTH_CONS pushes n+-1 into asms*) |
187 (*2nd NTH_CONS pushes n+-1 into asms*) |
188 Calc("Groups.plus_class.plus", 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}), |
202 Rls {id="srls_IntegrierenUnd..", |
202 Rls {id="srls_IntegrierenUnd..", |
203 preconds = [], |
203 preconds = [], |
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 ("Orderings.ord_class.less",eval_equ "#less_"), |
208 (*2nd NTH_CONS pushes n+-1 into asms*) |
208 (*2nd NTH_CONS pushes n+-1 into asms*) |
209 Calc("Groups.plus_class.plus", 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}), |