src/HOL/Set.thy
changeset 12633 ad9277743664
parent 12338 de0f4a63baa5
child 12897 f4d10ad0ea7b
--- 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 <")