diff -r 17db21aa9aed -r 73ee61385493 src/Tools/isac/Knowledge/LinEq.thy
--- a/src/Tools/isac/Knowledge/LinEq.thy	Mon Apr 19 20:44:18 2021 +0200
+++ b/src/Tools/isac/Knowledge/LinEq.thy	Tue Apr 20 16:58:44 2021 +0200
@@ -13,7 +13,7 @@
 (*-- normalise --*)
   (*WN0509 compare PolyEq.all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"*)
   all_left:          "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)" and
-  makex1_x:          "a^^^1  = a" and
+  makex1_x:          "a \<up> 1  = a" and
   real_assoc_1:      "a+(b+c) = a+b+c" and
   real_assoc_2:      "a*(b*c) = a*b*c" and