1.1 --- a/src/sml/IsacKnowledge/Integrate.ML	Sat Aug 20 18:04:54 2005 +0200
     1.2 +++ b/src/sml/IsacKnowledge/Integrate.ML	Sat Aug 20 18:25:14 2005 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4   ("integral_var",num_str integral_var),
     1.5   ("integral_add",num_str integral_add),
     1.6   ("integral_mult",num_str integral_mult),
     1.7 - ("add_new_c",num_str add_new_c),
     1.8 + ("call_for_new_c",num_str call_for_new_c),
     1.9   ("integral_pow",num_str integral_pow)
    1.10  ]);
    1.11  
    1.12 @@ -81,6 +81,22 @@
    1.13  			    Calc ("op +", eval_binop "#add_")(*for n+1*)
    1.14  			    ],
    1.15  		   scr = EmptyScr});
    1.16 +val add_new_c = 
    1.17 +    prep_rls (Seq {id="add_new_c", preconds = [], 
    1.18 +		   rew_ord = ("termlessI",termlessI), 
    1.19 +		   erls = Rls {id="conditions_in_add_new_c", 
    1.20 +			       preconds = [], 
    1.21 +			       rew_ord = ("termlessI",termlessI), 
    1.22 +			       erls = Erls, 
    1.23 +			       srls = Erls, calc = [],
    1.24 +			       rules = [Calc ("Tools.matches", eval_matches "")
    1.25 +					],
    1.26 +			       scr = EmptyScr}, 
    1.27 +		   srls = Erls, calc = [],
    1.28 +		   rules = [ Thm ("call_for_new_c", num_str call_for_new_c),
    1.29 +			     Calc("Integrate.new'_c", eval_new_c "new_c_")
    1.30 +			    ],
    1.31 +		   scr = EmptyScr});
    1.32  val integration = 
    1.33      prep_rls (Seq {id="integration", preconds = [], 
    1.34  		   rew_ord = ("termlessI",termlessI), 
    1.35 @@ -89,16 +105,16 @@
    1.36  			       rew_ord = ("termlessI",termlessI), 
    1.37  			       erls = Erls, 
    1.38  			       srls = Erls, calc = [],
    1.39 -			       rules = [Calc ("Tools.matches", eval_matches "")
    1.40 -					],
    1.41 +			       rules = [],
    1.42  			       scr = EmptyScr}, 
    1.43  		   srls = Erls, calc = [],
    1.44  		   rules = [ Rls_ integration_rules,
    1.45 -			     Thm ("add_new_c",num_str add_new_c),
    1.46 -			     Calc ("Integrate.new'_c", eval_new_c "new_c_")
    1.47 +			     Rls_ add_new_c,
    1.48 +			     Rls_ norm_Poly
    1.49  			    ],
    1.50  		   scr = EmptyScr});
    1.51  ruleset' := overwritel (!ruleset', [("integration_rules", integration_rules),
    1.52 +				    ("add_new_c", add_new_c),
    1.53  				    ("integration", integration)]);
    1.54  
    1.55  (** problems **)

     2.1 --- a/src/sml/IsacKnowledge/Integrate.thy	Sat Aug 20 18:04:54 2005 +0200
     2.2 +++ b/src/sml/IsacKnowledge/Integrate.thy	Sat Aug 20 18:25:14 2005 +0200
     2.3 @@ -43,7 +43,7 @@
     2.4  		    \(Integral u D bdv) + (Integral v D bdv)"
     2.5    integral_mult     "[| Not (bdv occurs_in u); bdv occurs_in v |] ==> \
     2.6  		    \Integral (u * v) D bdv = u * (Integral v D bdv)"
     2.7 -  add_new_c         "Not (matches (u + new_c v) a) ==> a = a + new_c a"
     2.8 +  call_for_new_c    "Not (matches (u + new_c v) a) ==> a = a + new_c a"
     2.9  
    2.10    integral_pow      "Integral bdv ^^^ n D bdv = bdv ^^^ (n+1) / (n + 1)"
    2.11  

     3.1 --- a/src/smltest/IsacKnowledge/integrate.sml	Sat Aug 20 18:04:54 2005 +0200
     3.2 +++ b/src/smltest/IsacKnowledge/integrate.sml	Sat Aug 20 18:25:14 2005 +0200
     3.3 @@ -109,8 +109,8 @@
     3.4  (*
     3.5  trace_rewrite := true;
     3.6  *)
     3.7 -val str = rewrit add_new_c (str2t "x ^^^ 2 / 2"); term2s str;
     3.8 -val str = (rewrit add_new_c str)
     3.9 +val str = rewrit call_for_new_c (str2t "x ^^^ 2 / 2"); term2s str;
    3.10 +val str = (rewrit call_for_new_c str)
    3.11      handle OPTION =>  str2t "no_rewrite";;
    3.12  
    3.13  (*