diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/IsacKnowledge/Integrate.thy
--- a/src/Tools/isac/IsacKnowledge/Integrate.thy	Wed Aug 25 15:15:01 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,54 +0,0 @@
-(* integration over the reals
-   author: Walther Neuper
-   050814, 08:51
-   (c) due to copyright terms
-
-remove_thy"Integrate";
-use_thy"IsacKnowledge/Integrate";
-use_thy_only"IsacKnowledge/Integrate";
-
-remove_thy"Typefix";
-use_thy"IsacKnowledge/Isac";
-*)
-
-Integrate = Diff +
-
-consts
-
-  Integral            :: "[real, real]=> real" ("Integral _ D _" 91)
-(*new'_c	      :: "real => real"        ("new'_c _" 66)*)
-  is'_f'_x            :: "real => bool"        ("_ is'_f'_x" 10)
-
-  (*descriptions in the related problems*)
-  integrateBy         :: real => una
-  antiDerivative      :: real => una
-  antiDerivativeName  :: (real => real) => una
-
-  (*the CAS-command, eg. "Integrate (2*x^^^3, x)"*)
-  Integrate           :: "[real * real] => real"
-
-  (*Script-names*)
-  IntegrationScript      :: "[real,real,  real] => real"
-                  ("((Script IntegrationScript (_ _ =))// (_))" 9)
-  NamedIntegrationScript :: "[real,real, real=>real,  bool] => bool"
-                  ("((Script NamedIntegrationScript (_ _ _=))// (_))" 9)
-
-rules 
-(*stated as axioms, todo: prove as theorems
-  'bdv' is a constant handled on the meta-level 
-   specifically as a 'bound variable'            *)
-
-  integral_const    "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv"
-  integral_var      "Integral bdv D bdv = bdv ^^^ 2 / 2"
-
-  integral_add      "Integral (u + v) D bdv = \
-		    \(Integral u D bdv) + (Integral v D bdv)"
-  integral_mult     "[| Not (bdv occurs_in u); bdv occurs_in v |] ==> \
-		    \Integral (u * v) D bdv = u * (Integral v D bdv)"
-(*WN080222: this goes into sub-terms, too ...
-  call_for_new_c    "[| Not (matches (u + new_c v) a); Not (a is_f_x) |] ==> \
-		    \a = a + new_c a"
-*)
-  integral_pow      "Integral bdv ^^^ n D bdv = bdv ^^^ (n+1) / (n + 1)"
-
-end
\ No newline at end of file