1.1 --- a/src/sml/IsacKnowledge/Integrate.ML	Sat Aug 20 13:00:20 2005 +0200
     1.2 +++ b/src/sml/IsacKnowledge/Integrate.ML	Sat Aug 20 15:15:41 2005 +0200
     1.3 @@ -50,20 +50,8 @@
     1.4  	  Trueprop $ (mk_equality (p, new_c p)))
     1.5    | eval_new_c _ _ _ _ = None;
     1.6  
     1.7 -(*("is_new_c_free", ("Integrate.is'_new'_c'_free", eval_is_new_c_free ""))*)
     1.8 -fun eval_is_new_c_free _ _ 
     1.9 -		       (p as (Const ("Integrate.is'_new'_c'_free",_) $ t)) _ =
    1.10 -    if contains_term t (Const ("Integrate.new'_c", 
    1.11 -			       HOLogic.realT-->HOLogic.realT))
    1.12 -    then Some ((term2str p) ^ " = False",
    1.13 -	       Trueprop $ (mk_equality (p, HOLogic.false_const)))
    1.14 -    else Some ((term2str p) ^ " = True",
    1.15 -	       Trueprop $ (mk_equality (p, HOLogic.true_const)))
    1.16 -  | eval_is_new_c_free _ _ _  _ = None;
    1.17 -
    1.18  calclist':= overwritel (!calclist', 
    1.19 -   [("new_c", ("Integrate.new'_c", eval_new_c "new_c_")),
    1.20 -    ("is_new_c_free", ("Integrate.is'_new'_c'_free", eval_is_new_c_free ""))
    1.21 +   [("new_c", ("Integrate.new'_c", eval_new_c "new_c_"))
    1.22      ]);
    1.23  
    1.24  (** rulesets **)
    1.25 @@ -101,8 +89,7 @@
    1.26  			       rew_ord = ("termlessI",termlessI), 
    1.27  			       erls = Erls, 
    1.28  			       srls = Erls, calc = [],
    1.29 -			       rules = [Calc ("Integrate.is'_new'_c'_free", 
    1.30 -					      eval_is_new_c_free "")
    1.31 +			       rules = [Calc ("Tools.matches", eval_matches "")
    1.32  					],
    1.33  			       scr = EmptyScr}, 
    1.34  		   srls = Erls, calc = [],

     2.1 --- a/src/sml/IsacKnowledge/Integrate.thy	Sat Aug 20 13:00:20 2005 +0200
     2.2 +++ b/src/sml/IsacKnowledge/Integrate.thy	Sat Aug 20 15:15:41 2005 +0200
     2.3 @@ -3,11 +3,11 @@
     2.4     050814, 08:51
     2.5     (c) due to copyright terms
     2.6  
     2.7 -remove_thy"Typefix";
     2.8  remove_thy"Integrate";
     2.9 -
    2.10  use_thy"~/proto2/isac/src/sml/IsacKnowledge/Integrate";
    2.11  use_thy_only"~/proto2/isac/src/sml/IsacKnowledge/Integrate";
    2.12 +
    2.13 +remove_thy"Typefix";
    2.14  use_thy"~/proto2/isac/src/sml/IsacKnowledge/Isac";
    2.15  *)
    2.16  
    2.17 @@ -17,7 +17,6 @@
    2.18  
    2.19    Integral         :: "[real, real]=> real"    ("Integral _ D _" 91)
    2.20    new'_c	   :: "real => real"           ("new'_c _" 66)
    2.21 -  is'_new'_c'_free :: "real => bool"           ("_ is'_new'_c'_free" 66)
    2.22  
    2.23    (*new Descriptions in the problem*)
    2.24    integrateBy      :: real => una
    2.25 @@ -37,17 +36,13 @@
    2.26    'bdv' is a constant handled on the meta-level 
    2.27     specifically as a 'bound variable'            *)
    2.28  
    2.29 -  integral_const    "[| Not (bdv occurs_in u) |] ==> \
    2.30 -		    \Integral u D bdv = u * bdv"
    2.31 +  integral_const    "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv"
    2.32    integral_var      "Integral bdv D bdv = bdv ^^^ 2 / 2"
    2.33  
    2.34    integral_add      "Integral (u + v) D bdv = \
    2.35  		    \(Integral u D bdv) + (Integral v D bdv)"
    2.36    integral_mult     "[| Not (bdv occurs_in u); bdv occurs_in v |] ==> \
    2.37  		    \Integral (u * v) D bdv = u * (Integral v D bdv)"
    2.38 -(*
    2.39 -  add_new_c         "a is_new_c_free ==> a = a + new_c a"
    2.40 -*)
    2.41    add_new_c         "Not (matches (u + new_c v) a) ==> a = a + new_c a"
    2.42  
    2.43    integral_pow      "Integral bdv ^^^ n D bdv = bdv ^^^ (n+1) / (n + 1)"