1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Tue Oct 05 14:41:16 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Tue Oct 05 15:28:32 2010 +0200
     1.3 @@ -361,7 +361,7 @@
     1.4  		     rew_ord = ("e_rew_ord", e_rew_ord), 
     1.5  		     erls = Erls, srls = Erls, calc = [],
     1.6  		     rules = [(*for precond NTH_CONS ...*)
     1.7 -			      Calc ("op <",eval_equ "#less_"),
     1.8 +			      Calc ("Orderings.ord_class.less",eval_equ "#less_"),
     1.9  			      Calc ("Groups.plus_class.plus", eval_binop "#add_")
    1.10  			      (*immediately repeated rewrite pushes
    1.11  					    '+' into precondition !*)
    1.12 @@ -390,7 +390,7 @@
    1.13  		     rew_ord = ("e_rew_ord", e_rew_ord), 
    1.14  		     erls = Erls, srls = Erls, calc = [],
    1.15  		     rules = [(*for precond NTH_CONS ...*)
    1.16 -			      Calc ("op <",eval_equ "#less_"),
    1.17 +			      Calc ("Orderings.ord_class.less",eval_equ "#less_"),
    1.18  			      Calc ("Groups.plus_class.plus", eval_binop "#add_")
    1.19  			      (*immediately repeated rewrite pushes
    1.20  					    '+' into precondition !*)
    1.21 @@ -670,7 +670,7 @@
    1.22  		rew_ord = ("termlessI",termlessI), 
    1.23  		erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
    1.24  				  [(*for asm in NTH_CONS ...*)
    1.25 -				   Calc ("op <",eval_equ "#less_"),
    1.26 +				   Calc ("Orderings.ord_class.less",eval_equ "#less_"),
    1.27  				   (*2nd NTH_CONS pushes n+-1 into asms*)
    1.28  				   Calc("Groups.plus_class.plus", eval_binop "#add_")
    1.29  				   ],