1.1 --- a/test/Tools/isac/Knowledge/biegelinie.sml Thu Sep 23 12:56:51 2010 +0200
1.2 +++ b/test/Tools/isac/Knowledge/biegelinie.sml Thu Sep 23 14:49:23 2010 +0200
1.3 @@ -142,11 +142,11 @@
1.4 [(*for asm in nth_Cons_ ...*)
1.5 Calc ("op <",eval_equ "#less_"),
1.6 (*2nd nth_Cons_ pushes n+-1 into asms*)
1.7 - Calc("op +", eval_binop "#add_")
1.8 + Calc("Groups.plus_class.plus", eval_binop "#add_")
1.9 ],
1.10 srls = Erls, calc = [],
1.11 rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}),
1.12 - Calc("op +", eval_binop "#add_"),
1.13 + Calc("Groups.plus_class.plus", eval_binop "#add_"),
1.14 Thm ("nth_Nil_",num_str @{thm nth_Nil_}),
1.15 Calc("Tools.lhs", eval_lhs"eval_lhs_"),
1.16 Calc("Tools.rhs", eval_rhs"eval_rhs_"),