--- a/src/HOL/HOL.thy Tue May 20 10:48:08 1997 +0200
+++ b/src/HOL/HOL.thy Tue May 20 11:05:59 1997 +0200
@@ -25,6 +25,10 @@
bool :: term
+syntax ("" output)
+ "op =" :: ['a, 'a] => bool ("(_ =/ _)" [51, 51] 50)
+ "op ~=" :: ['a, 'a] => bool ("(_ ~=/ _)" [51, 51] 50)
+
consts
(* Constants *)
@@ -110,6 +114,8 @@
"_Let (_binds b bs) e" == "_Let b (_Let bs e)"
"let x = a in e" == "Let a (%x. e)"
+syntax (symbols output)
+ "op ~=" :: ['a, 'a] => bool ("(_ \\<noteq>/ _)" [51, 51] 50)
syntax (symbols)
Not :: bool => bool ("\\<not> _" [40] 40)