1.1 --- a/src/Tools/isac/Knowledge/RatEq.thy	Mon Sep 06 15:53:18 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy	Mon Sep 06 16:56:22 2010 +0200
     1.3 @@ -24,28 +24,22 @@
     1.4     (* FIXME also in Poly.thy def. --> FIXED*)
     1.5     (*real_diff_minus            
     1.6     "a - b = a + (-1) * b"*)
     1.7 -   real_rat_mult_1
     1.8 -   "a*(b/c) = (a*b)/c"
     1.9 -   real_rat_mult_2
    1.10 -   "(a/b)*(c/d) = (a*c)/(b*d)"
    1.11 -   real_rat_mult_3
    1.12 -   "(a/b)*c = (a*c)/b"
    1.13 -   real_rat_pow
    1.14 -   "(a/b)^^^2 = a^^^2/b^^^2"
    1.15 +   real_rat_mult_1:   "a*(b/c) = (a*b)/c"
    1.16 +   real_rat_mult_2:   "(a/b)*(c/d) = (a*c)/(b*d)"
    1.17 +   real_rat_mult_3:   "(a/b)*c = (a*c)/b"
    1.18 +   real_rat_pow:      "(a/b)^^^2 = a^^^2/b^^^2"
    1.19  
    1.20 -   rat_double_rat_1
    1.21 -   "[|Not(c=0); Not(d=0)|] ==> (a / (c/d) = (a*d) / c)"
    1.22 -   rat_double_rat_2
    1.23 -   "[|Not(b=0);Not(c=0); Not(d=0)|] ==> ((a/b) / (c/d) = (a*d) / (b*c))"
    1.24 -   rat_double_rat_3
    1.25 -   "[|Not(b=0);Not(c=0)|] ==> ((a/b) / c = a / (b*c))"
    1.26 +   rat_double_rat_1:   "[|Not(c=0); Not(d=0)|] ==> (a / (c/d) = (a*d) / c)"
    1.27 +   rat_double_rat_2:   "[|Not(b=0);Not(c=0); Not(d=0)|] ==> 
    1.28 +                                           ((a/b) / (c/d) = (a*d) / (b*c))"
    1.29 +   rat_double_rat_3:   "[|Not(b=0);Not(c=0)|] ==> ((a/b) / c = a / (b*c))"
    1.30  
    1.31    (* equation to same denominator *)
    1.32 -  rat_mult_denominator_both
    1.33 +  rat_mult_denominator_both:
    1.34     "[|Not(b=0); Not(d=0)|] ==> ((a::real) / b = c / d) = (a*d = c*b)"
    1.35 -  rat_mult_denominator_left
    1.36 +  rat_mult_denominator_left:
    1.37     "[|Not(d=0)|] ==> ((a::real) = c / d) = (a*d = c)"
    1.38 -  rat_mult_denominator_right
    1.39 +  rat_mult_denominator_right:
    1.40     "[|Not(b=0)|] ==> ((a::real) / b = c) = (a = c*b)"
    1.41  
    1.42  ML {*