1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Thu Sep 23 12:56:51 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Thu Sep 23 14:49:23 2010 +0200
     1.3 @@ -140,7 +140,7 @@
     1.4  		  Thm ("integral_add",num_str @{thm integral_add}),
     1.5  		  Thm ("integral_mult",num_str @{thm integral_mult}),
     1.6  		  Thm ("integral_pow",num_str @{thm integral_pow}),
     1.7 -		  Calc ("op +", eval_binop "#add_")(*for n+1*)
     1.8 +		  Calc ("Groups.plus_class.plus", eval_binop "#add_")(*for n+1*)
     1.9  		  ],
    1.10  	 scr = EmptyScr};
    1.11  *}
    1.12 @@ -200,7 +200,7 @@
    1.13  	       Thm ("divide_divide_eq_left",
    1.14                       num_str @{thm divide_divide_eq_left}),
    1.15  	       (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
    1.16 -	       Calc ("HOL.divide"  ,eval_cancel "#divide_e"),
    1.17 +	       Calc ("Rings.inverse_class.divide"  ,eval_cancel "#divide_e"),
    1.18  	      
    1.19  	       Thm ("rat_power", num_str @{thm rat_power})
    1.20  		(*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
    1.21 @@ -264,7 +264,7 @@
    1.22  	       Rls_ discard_parentheses,
    1.23  	       (*Rls_ collect_bdv, from make_polynomial_in*)
    1.24  	       Rls_ separate_bdv2,
    1.25 -	       Calc ("HOL.divide"  ,eval_cancel "#divide_e")
    1.26 +	       Calc ("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")
    1.27  	       ],
    1.28        scr = EmptyScr}:rls;      
    1.29  
    1.30 @@ -302,7 +302,7 @@
    1.31  * 				 num_str @{thm add_divide_distrib})
    1.32  * 			   (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
    1.33  * 			  ]),
    1.34 -* 	       Calc ("HOL.divide"  ,eval_cancel "#divide_e")
    1.35 +* 	       Calc ("Rings.inverse_class.divide"  ,eval_cancel "#divide_e")
    1.36  * 	       ],
    1.37  *       scr = EmptyScr
    1.38  *       }:rls);