# HG changeset patch
# User wenzelm
# Date 864119159 -7200
# Node ID 3772723c5e413551a098fee3b9967949e742152d
# Parent  cb3c27f2753eb83a261b997649edeb478de75459
improved output syntax of op =, op ~= (more parentheses);

diff -r cb3c27f2753e -r 3772723c5e41 src/HOL/HOL.thy
--- 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)