src/ZF/OrdQuant.thy
changeset 12114 a8e860c86252
parent 6093 87bf8c03b169
child 12552 d2d2ab3f1f37
--- a/src/ZF/OrdQuant.thy	Fri Nov 09 00:06:15 2001 +0100
+++ b/src/ZF/OrdQuant.thy	Fri Nov 09 00:09:47 2001 +0100
@@ -25,7 +25,7 @@
   "EX x<a. P"   == "oex(a, %x. P)"
   "UN x<a. B"   == "OUnion(a, %x. B)"
 
-syntax (symbols)
+syntax (xsymbols)
   "@oall"     :: [idt, i, o] => o        ("(3\\<forall> _<_./ _)" 10)
   "@oex"      :: [idt, i, o] => o        ("(3\\<exists> _<_./ _)" 10)
   "@OUNION"   :: [idt, i, i] => i        ("(3\\<Union> _<_./ _)" 10)