1.1 --- a/src/Tools/isac/IsacKnowledge/Integrate.thy	Wed Aug 25 15:15:01 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,54 +0,0 @@
     1.4 -(* integration over the reals
     1.5 -   author: Walther Neuper
     1.6 -   050814, 08:51
     1.7 -   (c) due to copyright terms
     1.8 -
     1.9 -remove_thy"Integrate";
    1.10 -use_thy"IsacKnowledge/Integrate";
    1.11 -use_thy_only"IsacKnowledge/Integrate";
    1.12 -
    1.13 -remove_thy"Typefix";
    1.14 -use_thy"IsacKnowledge/Isac";
    1.15 -*)
    1.16 -
    1.17 -Integrate = Diff +
    1.18 -
    1.19 -consts
    1.20 -
    1.21 -  Integral            :: "[real, real]=> real" ("Integral _ D _" 91)
    1.22 -(*new'_c	      :: "real => real"        ("new'_c _" 66)*)
    1.23 -  is'_f'_x            :: "real => bool"        ("_ is'_f'_x" 10)
    1.24 -
    1.25 -  (*descriptions in the related problems*)
    1.26 -  integrateBy         :: real => una
    1.27 -  antiDerivative      :: real => una
    1.28 -  antiDerivativeName  :: (real => real) => una
    1.29 -
    1.30 -  (*the CAS-command, eg. "Integrate (2*x^^^3, x)"*)
    1.31 -  Integrate           :: "[real * real] => real"
    1.32 -
    1.33 -  (*Script-names*)
    1.34 -  IntegrationScript      :: "[real,real,  real] => real"
    1.35 -                  ("((Script IntegrationScript (_ _ =))// (_))" 9)
    1.36 -  NamedIntegrationScript :: "[real,real, real=>real,  bool] => bool"
    1.37 -                  ("((Script NamedIntegrationScript (_ _ _=))// (_))" 9)
    1.38 -
    1.39 -rules 
    1.40 -(*stated as axioms, todo: prove as theorems
    1.41 -  'bdv' is a constant handled on the meta-level 
    1.42 -   specifically as a 'bound variable'            *)
    1.43 -
    1.44 -  integral_const    "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv"
    1.45 -  integral_var      "Integral bdv D bdv = bdv ^^^ 2 / 2"
    1.46 -
    1.47 -  integral_add      "Integral (u + v) D bdv = \
    1.48 -		    \(Integral u D bdv) + (Integral v D bdv)"
    1.49 -  integral_mult     "[| Not (bdv occurs_in u); bdv occurs_in v |] ==> \
    1.50 -		    \Integral (u * v) D bdv = u * (Integral v D bdv)"
    1.51 -(*WN080222: this goes into sub-terms, too ...
    1.52 -  call_for_new_c    "[| Not (matches (u + new_c v) a); Not (a is_f_x) |] ==> \
    1.53 -		    \a = a + new_c a"
    1.54 -*)
    1.55 -  integral_pow      "Integral bdv ^^^ n D bdv = bdv ^^^ (n+1) / (n + 1)"
    1.56 -
    1.57 -end
    1.58 \ No newline at end of file