diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/Knowledge/RootRatEq.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Wed Aug 25 16:20:07 2010 +0200
@@ -0,0 +1,48 @@
+(*.c) by Richard Lang, 2003 .*)
+(* collecting all knowledge for Root and Rational Equations
+   created by: rlang 
+         date: 02.10
+   changed by: rlang
+   last change by: rlang
+             date: 02.11.04
+*)
+
+(* use"knowledge/RootRatEq.ML";
+   use"RootRatEq.ML";
+
+   use"ROOT.ML";
+   cd"knowledge";
+
+   remove_thy"RootRatEq";
+   use_thy"Isac";
+   *)
+
+RootRatEq = RootEq + RatEq + RootRat + 
+
+(*-------------------- consts-----------------------------------------------*)
+consts
+
+  is'_rootRatAddTerm'_in :: [real, real] => bool ("_ is'_rootRatAddTerm'_in _") (*RL DA*)
+
+(*---------scripts--------------------------*)
+  Elim'_rootrat'_equation
+             :: "[bool,real, \
+		  \ bool list] => bool list"
+               ("((Script Elim'_rootrat'_equation (_ _ =))// \
+                 \ (_))" 9)
+ (*-------------------- rules------------------------------------------------*)
+rules
+
+  (* eliminate ratRootTerm *)
+  rootrat_equation_left_1
+   "[|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c ))"
+  rootrat_equation_left_2
+   "[|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c ))"
+  rootrat_equation_right_2
+   "[|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e ))"
+  rootrat_equation_right_1
+   "[|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))"
+
+
+
+end