# HG changeset patch
# User wenzelm
# Date 1010168970 -3600
# Node ID ad9277743664a0b9ec1396eec86115bba52d7610
# Parent  3d3e356778b53f0f8a4f8314efdecb79fc03e1e3
tuned ``syntax (output)'';

diff -r 3d3e356778b5 -r ad9277743664 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Jan 04 19:28:57 2002 +0100
+++ b/src/HOL/HOL.thy	Fri Jan 04 19:29:30 2002 +0100
@@ -75,7 +75,7 @@
   "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
   "let x = a in e"        == "Let a (%x. e)"
 
-syntax ("" output)
+syntax (output)
   "="           :: "['a, 'a] => bool"                    (infix 50)
   "~="          :: "['a, 'a] => bool"                    (infix 50)
 
diff -r 3d3e356778b5 -r ad9277743664 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Jan 04 19:28:57 2002 +0100
+++ b/src/HOL/Set.thy	Fri Jan 04 19:29:30 2002 +0100
@@ -85,7 +85,7 @@
   "ALL x:A. P"  == "Ball A (%x. P)"
   "EX x:A. P"   == "Bex A (%x. P)"
 
-syntax ("" output)
+syntax (output)
   "_setle"      :: "'a set => 'a set => bool"             ("op <=")
   "_setle"      :: "'a set => 'a set => bool"             ("(_/ <= _)" [50, 51] 50)
   "_setless"    :: "'a set => 'a set => bool"             ("op <")