diff -r d199410f1db1 -r 968d2dccf2de hol.thy
--- a/hol.thy	Mon Oct 04 15:43:54 1993 +0100
+++ b/hol.thy	Thu Oct 07 10:20:30 1993 +0100
@@ -54,7 +54,7 @@
   (* Infixes *)
 
   o             :: "['b => 'c, 'a => 'b, 'a] => 'c"   (infixr 50)
-  "="           :: "['a, 'a] => bool"                 (infixl 50)
+  "=", "~="     :: "['a, 'a] => bool"                 (infixl 50)
   "&"           :: "[bool, bool] => bool"             (infixr 35)
   "|"           :: "[bool, bool] => bool"             (infixr 30)
   "-->"         :: "[bool, bool] => bool"             (infixr 25)
@@ -65,10 +65,6 @@
   "-"           :: "['a::minus, 'a] => 'a"            (infixl 65)
   "*"           :: "['a::times, 'a] => 'a"            (infixl 70)
 
-  (* Rewriting Gadget *)
-
-  NORM          :: "'a => 'a"
-
 
 translations
   "THE xs. P"   => "@ xs. P"
@@ -76,6 +72,7 @@
   "EX xs. P"    => "? xs. P"
   "EX! xs. P"   => "?! xs. P"
 
+  "x ~= y"         == "~ (x=y)"
   "let x = s in t" == "Let(s, %x. t)"
 
 rules
@@ -116,10 +113,6 @@
 
   if_def        "if = (%P x y.@z::'a. (P=True --> z=x) & (P=False --> z=y))"
 
-  (* Rewriting -- special constant to flag normalized terms *)
-
-  NORM_def      "NORM(x) = x"
-
 end