1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Wed Sep 08 16:45:27 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Wed Sep 08 16:47:22 2010 +0200
     1.3 @@ -241,8 +241,8 @@
     1.4  		(*"?bdv / ?b = (1 / ?b) * ?bdv"*)
     1.5  		Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})(*,
     1.6  			  (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
     1.7 -			  *****Thm ("nadd_divide_distrib", 
     1.8 -			  *****num_str @{thm nadd_divide_distrib})
     1.9 +			  *****Thm ("add_divide_distrib", 
    1.10 +			  *****num_str @{thm add_divide_distrib})
    1.11  			  (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
    1.12  		];
    1.13  val simplify_Integral = 
    1.14 @@ -252,7 +252,7 @@
    1.15        calc = [], (*asm_thm = [],*)
    1.16        rules = [Thm ("left_distrib",num_str @{thm left_distrib}),
    1.17   	       (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
    1.18 -	       Thm ("nadd_divide_distrib",num_str @{thm nadd_divide_distrib}),
    1.19 +	       Thm ("add_divide_distrib",num_str @{thm add_divide_distrib}),
    1.20   	       (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
    1.21  	       (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
    1.22  	       Rls_ norm_Rational_noadd_fractions,
    1.23 @@ -294,8 +294,8 @@
    1.24  * 			  (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
    1.25  * 			  Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})(*,
    1.26  * 			  (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
    1.27 -* 			  Thm ("nadd_divide_distrib", 
    1.28 -* 				 num_str @{thm nadd_divide_distrib})
    1.29 +* 			  Thm ("add_divide_distrib", 
    1.30 +* 				 num_str @{thm add_divide_distrib})
    1.31  * 			   (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
    1.32  * 			  ]),
    1.33  * 	       Calc ("HOL.divide"  ,eval_cancel "#divide_e")
    1.34 @@ -369,7 +369,7 @@
    1.35  	     crls = Atools_erls, nrls = e_rls},
    1.36  "Script IntegrationScript (f_::real) (v_v::real) =                " ^
    1.37  "  (let t_ = Take (Integral f_ D v_v)                             " ^
    1.38 -"   in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))"
    1.39 +"   in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_::real))"
    1.40  ));
    1.41      
    1.42  store_met
    1.43 @@ -384,8 +384,8 @@
    1.44  		crls = Atools_erls, nrls = e_rls},
    1.45  "Script NamedIntegrationScript (f_::real) (v_v::real) (F_::real=>real) = " ^
    1.46  "  (let t_ = Take (F_ v_v = Integral f_ D v_v)                            " ^
    1.47 -"   in ((Try (Rewrite_Set_Inst [(bdv,v_)] simplify_Integral False)) @@  " ^
    1.48 -"       (Rewrite_Set_Inst [(bdv,v_)] integration False)) t_)            "
    1.49 +"   in ((Try (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) @@  " ^
    1.50 +"       (Rewrite_Set_Inst [(bdv,v_v)] integration False)) t_)            "
    1.51      ));
    1.52  *}
    1.53