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