diff -r 66f3570ba808 -r 03bfbc480107 src/Tools/isac/Knowledge/RootRatEq.thy
--- a/src/Tools/isac/Knowledge/RootRatEq.thy	Mon Sep 06 15:53:18 2010 +0200
+++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Mon Sep 06 16:56:22 2010 +0200
@@ -24,13 +24,13 @@
 
 axioms
   (* eliminate ratRootTerm *)
-  rootrat_equation_left_1
+  rootrat_equation_left_1:
    "[|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c ))"
-  rootrat_equation_left_2
+  rootrat_equation_left_2:
    "[|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c ))"
-  rootrat_equation_right_2
+  rootrat_equation_right_2:
    "[|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e ))"
-  rootrat_equation_right_1
+  rootrat_equation_right_1:
    "[|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))"
 
 ML {*