1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Mon Apr 19 20:44:18 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Tue Apr 20 16:58:44 2021 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  (*-- normalise --*)
     1.5    (*WN0509 compare PolyEq.all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"*)
     1.6    all_left:          "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)" and
     1.7 -  makex1_x:          "a^^^1  = a" and
     1.8 +  makex1_x:          "a \<up> 1  = a" and
     1.9    real_assoc_1:      "a+(b+c) = a+b+c" and
    1.10    real_assoc_2:      "a*(b*c) = a*b*c" and
    1.11