1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Thu Sep 23 12:56:51 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Thu Sep 23 14:49:23 2010 +0200
     1.3 @@ -185,11 +185,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_"),
    1.17 @@ -206,11 +206,11 @@
    1.18  			   [(*for asm in NTH_CONS ...*)
    1.19  			    Calc ("op <",eval_equ "#less_"),
    1.20  			    (*2nd NTH_CONS pushes n+-1 into asms*)
    1.21 -			    Calc("op +", eval_binop "#add_")
    1.22 +			    Calc("Groups.plus_class.plus", eval_binop "#add_")
    1.23  			    ], 
    1.24  	 srls = Erls, calc = [],
    1.25  	 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
    1.26 -		  Calc("op +", eval_binop "#add_"),
    1.27 +		  Calc("Groups.plus_class.plus", eval_binop "#add_"),
    1.28  		  Thm ("NTH_NIL", num_str @{thm NTH_NIL}),
    1.29  		  Calc("Tools.lhs", eval_lhs "eval_lhs_"),
    1.30  		  Calc("Atools.filter'_sameFunId",