--- 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