1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Thu Aug 29 13:52:47 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Tue Sep 03 12:40:27 2019 +0200
     1.3 @@ -118,8 +118,7 @@
     1.4  		     erls = Rule.Erls, 
     1.5  		     srls = Rule.Erls, calc = [], errpatts = [],
     1.6  		     rules = [(*for rewriting conditions in Thm's*)
     1.7 -			      Rule.Calc ("Atools.occurs'_in", 
     1.8 -				    eval_occurs_in "#occurs_in_"),
     1.9 +			      Rule.Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "#occurs_in_"),
    1.10  			      Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
    1.11  			      Rule.Thm ("not_false",@{thm not_false})
    1.12  			      ],
    1.13 @@ -131,7 +130,7 @@
    1.14  		  Rule.Thm ("integral_add", TermC.num_str @{thm integral_add}),
    1.15  		  Rule.Thm ("integral_mult", TermC.num_str @{thm integral_mult}),
    1.16  		  Rule.Thm ("integral_pow", TermC.num_str @{thm integral_pow}),
    1.17 -		  Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_")(*for n+1*)
    1.18 +		  Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")(*for n+1*)
    1.19  		  ],
    1.20  	 scr = Rule.EmptyScr};
    1.21  \<close>
    1.22 @@ -144,7 +143,7 @@
    1.23  		     rew_ord = ("termlessI",termlessI), 
    1.24  		     erls = Rule.Erls, 
    1.25  		     srls = Rule.Erls, calc = [], errpatts = [],
    1.26 -		     rules = [Rule.Calc ("Tools.matches", Tools.eval_matches""),
    1.27 +		     rules = [Rule.Calc ("Prog_Expr.matches", Prog_Expr.eval_matches""),
    1.28  			      Rule.Calc ("Integrate.is'_f'_x", 
    1.29  				    eval_is_f_x "is_f_x_"),
    1.30  			      Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
    1.31 @@ -191,7 +190,7 @@
    1.32  	       Rule.Thm ("divide_divide_eq_left",
    1.33                       TermC.num_str @{thm divide_divide_eq_left}),
    1.34  	       (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
    1.35 -	       Rule.Calc ("Rings.divide_class.divide"  ,eval_cancel "#divide_e"),
    1.36 +	       Rule.Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
    1.37  	      
    1.38  	       Rule.Thm ("rat_power", TermC.num_str @{thm rat_power})
    1.39  		(*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
    1.40 @@ -255,7 +254,7 @@
    1.41  	       Rule.Rls_ discard_parentheses,
    1.42  	       (*Rule.Rls_ collect_bdv, from make_polynomial_in*)
    1.43  	       Rule.Rls_ separate_bdv2,
    1.44 -	       Rule.Calc ("Rings.divide_class.divide"  ,eval_cancel "#divide_e")
    1.45 +	       Rule.Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
    1.46  	       ],
    1.47        scr = Rule.EmptyScr};      
    1.48  
    1.49 @@ -293,7 +292,7 @@
    1.50  * 				  TermC.num_str @{thm add_divide_distrib})
    1.51  * 			   (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
    1.52  * 			  ]),
    1.53 -* 	       Rule.Calc ("Rings.divide_class.divide"  ,eval_cancel "#divide_e")
    1.54 +* 	       Rule.Calc ("Rings.divide_class.divide"  , eval_cancel "#divide_e")
    1.55  * 	       ],
    1.56  *       scr = Rule.EmptyScr
    1.57  *       });