diff -r 7972e16d2dd3 -r fc1674026e20 hol.thy
--- a/hol.thy	Fri Oct 22 13:36:28 1993 +0100
+++ b/hol.thy	Mon Oct 25 14:35:17 1993 +0100
@@ -14,7 +14,8 @@
   minus < term
   times < term
 
-default term
+default
+  term
 
 types
   bool 0
@@ -53,7 +54,8 @@
   (* Infixes *)
 
   o             :: "['b => 'c, 'a => 'b, 'a] => 'c"   (infixr 50)
-  "=", "~="     :: "['a, 'a] => bool"                 (infixl 50)
+  "="           :: "['a, 'a] => bool"                 (infixl 50)
+  "~="          :: "['a, 'a] => bool"                 ("(_ ~=/ _)" [50, 51] 50)
   "&"           :: "[bool, bool] => bool"             (infixr 35)
   "|"           :: "[bool, bool] => bool"             (infixr 30)
   "-->"         :: "[bool, bool] => bool"             (infixr 25)
@@ -69,9 +71,9 @@
   "ALL xs. P"   => "! xs. P"
   "EX xs. P"    => "? xs. P"
   "EX! xs. P"   => "?! xs. P"
+  "x ~= y"      == "~ (x = y)"
+  "let x = s in t" == "Let(s, %x. t)"
 
-  "x ~= y"         == "~ (x=y)"
-  "let x = s in t" == "Let(s, %x. t)"
 
 rules