test/Tools/isac/Knowledge/biegelinie.sml
branchisac-update-Isa09-2
changeset 38014 3e11e3c2dc42
parent 37991 028442673981
child 38031 460c24a6a6ba
     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_"),