1.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy	Mon Sep 06 15:53:18 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Mon Sep 06 16:56:22 2010 +0200
     1.3 @@ -24,13 +24,13 @@
     1.4  
     1.5  axioms
     1.6    (* eliminate ratRootTerm *)
     1.7 -  rootrat_equation_left_1
     1.8 +  rootrat_equation_left_1:
     1.9     "[|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c ))"
    1.10 -  rootrat_equation_left_2
    1.11 +  rootrat_equation_left_2:
    1.12     "[|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c ))"
    1.13 -  rootrat_equation_right_2
    1.14 +  rootrat_equation_right_2:
    1.15     "[|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e ))"
    1.16 -  rootrat_equation_right_1
    1.17 +  rootrat_equation_right_1:
    1.18     "[|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))"
    1.19  
    1.20  ML {*