1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Thu Sep 23 12:56:51 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Thu Sep 23 14:49:23 2010 +0200
     1.3 @@ -274,7 +274,7 @@
     1.4  	       (*Rls_ discard_parentheses *3**),
     1.5  	       Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
     1.6  	       Rls_ separate_bdv2,
     1.7 -	       Calc ("HOL.divide"  ,eval_cancel "#divide_e")
     1.8 +	       Calc ("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")
     1.9  	       ],
    1.10        scr = EmptyScr}:rls;      
    1.11  *}
    1.12 @@ -292,7 +292,7 @@
    1.13  	       Rls_ discard_parentheses,
    1.14  	       Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
    1.15  	       Rls_ separate_bdv2,
    1.16 -	       Calc ("HOL.divide"  ,eval_cancel "#divide_e")
    1.17 +	       Calc ("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")
    1.18  	       ],
    1.19        scr = EmptyScr}:rls;      
    1.20  (*
    1.21 @@ -362,14 +362,14 @@
    1.22  		     erls = Erls, srls = Erls, calc = [],
    1.23  		     rules = [(*for precond NTH_CONS ...*)
    1.24  			      Calc ("op <",eval_equ "#less_"),
    1.25 -			      Calc ("op +", eval_binop "#add_")
    1.26 +			      Calc ("Groups.plus_class.plus", eval_binop "#add_")
    1.27  			      (*immediately repeated rewrite pushes
    1.28  					    '+' into precondition !*)
    1.29  			      ],
    1.30  		     scr = EmptyScr}, 
    1.31  	 srls = Erls, calc = [],
    1.32  	 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
    1.33 -		  Calc ("op +", eval_binop "#add_"),
    1.34 +		  Calc ("Groups.plus_class.plus", eval_binop "#add_"),
    1.35  		  Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
    1.36  		  Thm ("tl_Cons",num_str @{thm tl_Cons}),
    1.37  		  Thm ("tl_Nil",num_str @{thm tl_Nil}),
    1.38 @@ -391,14 +391,14 @@
    1.39  		     erls = Erls, srls = Erls, calc = [],
    1.40  		     rules = [(*for precond NTH_CONS ...*)
    1.41  			      Calc ("op <",eval_equ "#less_"),
    1.42 -			      Calc ("op +", eval_binop "#add_")
    1.43 +			      Calc ("Groups.plus_class.plus", eval_binop "#add_")
    1.44  			      (*immediately repeated rewrite pushes
    1.45  					    '+' into precondition !*)
    1.46  			      ],
    1.47  		     scr = EmptyScr}, 
    1.48  	 srls = Erls, calc = [],
    1.49  	 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
    1.50 -		  Calc ("op +", eval_binop "#add_"),
    1.51 +		  Calc ("Groups.plus_class.plus", eval_binop "#add_"),
    1.52  		  Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
    1.53  		  Thm ("tl_Cons",num_str @{thm tl_Cons}),
    1.54  		  Thm ("tl_Nil",num_str @{thm tl_Nil}),
    1.55 @@ -458,7 +458,7 @@
    1.56    append_rls "prls_2x2_linear_system" e_rls 
    1.57  			     [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
    1.58  			      Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
    1.59 -			      Calc ("op +", eval_binop "#add_"),
    1.60 +			      Calc ("Groups.plus_class.plus", eval_binop "#add_"),
    1.61  			      Calc ("op =",eval_equal "#equal_")
    1.62  			      ], 
    1.63    SOME "solveSystem e_s v_s", 
    1.64 @@ -497,7 +497,7 @@
    1.65    append_rls "prls_3x3_linear_system" e_rls 
    1.66  			     [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
    1.67  			      Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
    1.68 -			      Calc ("op +", eval_binop "#add_"),
    1.69 +			      Calc ("Groups.plus_class.plus", eval_binop "#add_"),
    1.70  			      Calc ("op =",eval_equal "#equal_")
    1.71  			      ], 
    1.72    SOME "solveSystem e_s v_s", 
    1.73 @@ -513,7 +513,7 @@
    1.74    append_rls "prls_4x4_linear_system" e_rls 
    1.75  			     [Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS}),
    1.76  			      Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL}),
    1.77 -			      Calc ("op +", eval_binop "#add_"),
    1.78 +			      Calc ("Groups.plus_class.plus", eval_binop "#add_"),
    1.79  			      Calc ("op =",eval_equal "#equal_")
    1.80  			      ], 
    1.81    SOME "solveSystem e_s v_s", 
    1.82 @@ -672,11 +672,11 @@
    1.83  				  [(*for asm in NTH_CONS ...*)
    1.84  				   Calc ("op <",eval_equ "#less_"),
    1.85  				   (*2nd NTH_CONS pushes n+-1 into asms*)
    1.86 -				   Calc("op +", eval_binop "#add_")
    1.87 +				   Calc("Groups.plus_class.plus", eval_binop "#add_")
    1.88  				   ], 
    1.89  		srls = Erls, calc = [],
    1.90  		rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
    1.91 -			 Calc("op +", eval_binop "#add_"),
    1.92 +			 Calc("Groups.plus_class.plus", eval_binop "#add_"),
    1.93  			 Thm ("NTH_NIL",num_str @{thm NTH_NIL})],
    1.94  		scr = EmptyScr};
    1.95  store_met