diff -r 4e569846524c -r aabc6c8e930a src/Tools/isac/Knowledge/LinEq.thy
--- a/src/Tools/isac/Knowledge/LinEq.thy	Fri Oct 18 14:36:51 2013 +0200
+++ b/src/Tools/isac/Knowledge/LinEq.thy	Mon Oct 21 09:03:50 2013 +0200
@@ -16,17 +16,17 @@
                ("((Script Solve'_lineq'_equation (_ _ =))// 
                   (_))" 9)
 
-axioms(*axiomatization where*)
+axiomatization where
 (*-- normalize --*)
   (*WN0509 compare PolyEq.all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"*)
-  all_left:          "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)" 
-  makex1_x:          "a^^^1  = a"   
-  real_assoc_1:      "a+(b+c) = a+b+c" 
-  real_assoc_2:      "a*(b*c) = a*b*c" 
+  all_left:          "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)" and
+  makex1_x:          "a^^^1  = a" and
+  real_assoc_1:      "a+(b+c) = a+b+c" and
+  real_assoc_2:      "a*(b*c) = a*b*c" and
 
 (*-- solve --*)
-  lin_isolate_add1:  "(a + b*bdv = 0) = (b*bdv = (-1)*a)" 
-  lin_isolate_add2:  "(a +   bdv = 0) = (  bdv = (-1)*a)" 
+  lin_isolate_add1:  "(a + b*bdv = 0) = (b*bdv = (-1)*a)" and
+  lin_isolate_add2:  "(a +   bdv = 0) = (  bdv = (-1)*a)" and
   lin_isolate_div:   "[|Not(b=0)|] ==> (b*bdv = c) = (bdv = c / b)"
 
 ML {*