1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Tue Feb 13 16:17:59 2018 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Wed Feb 14 06:06:27 2018 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4                 ("((Script Solve'_lineq'_equation (_ _ =))// (_))" 9)
     1.5  
     1.6  axiomatization where
     1.7 -(*-- normalize --*)
     1.8 +(*-- normalise --*)
     1.9    (*WN0509 compare PolyEq.all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"*)
    1.10    all_left:          "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)" and
    1.11    makex1_x:          "a^^^1  = a" and