1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Fri Oct 18 14:36:51 2013 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Mon Oct 21 09:03:50 2013 +0200
     1.3 @@ -16,17 +16,17 @@
     1.4                 ("((Script Solve'_lineq'_equation (_ _ =))// 
     1.5                    (_))" 9)
     1.6  
     1.7 -axioms(*axiomatization where*)
     1.8 +axiomatization where
     1.9  (*-- normalize --*)
    1.10    (*WN0509 compare PolyEq.all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"*)
    1.11 -  all_left:          "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)" 
    1.12 -  makex1_x:          "a^^^1  = a"   
    1.13 -  real_assoc_1:      "a+(b+c) = a+b+c" 
    1.14 -  real_assoc_2:      "a*(b*c) = a*b*c" 
    1.15 +  all_left:          "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)" and
    1.16 +  makex1_x:          "a^^^1  = a" and
    1.17 +  real_assoc_1:      "a+(b+c) = a+b+c" and
    1.18 +  real_assoc_2:      "a*(b*c) = a*b*c" and
    1.19  
    1.20  (*-- solve --*)
    1.21 -  lin_isolate_add1:  "(a + b*bdv = 0) = (b*bdv = (-1)*a)" 
    1.22 -  lin_isolate_add2:  "(a +   bdv = 0) = (  bdv = (-1)*a)" 
    1.23 +  lin_isolate_add1:  "(a + b*bdv = 0) = (b*bdv = (-1)*a)" and
    1.24 +  lin_isolate_add2:  "(a +   bdv = 0) = (  bdv = (-1)*a)" and
    1.25    lin_isolate_div:   "[|Not(b=0)|] ==> (b*bdv = c) = (bdv = c / b)"
    1.26  
    1.27  ML {*