src/HOL/Set.thy
changeset 2372 a2999e19703b
parent 2368 d394336997cf
child 2388 d1f0505fc602
--- a/src/HOL/Set.thy	Tue Dec 10 15:08:57 1996 +0100
+++ b/src/HOL/Set.thy	Tue Dec 10 15:13:53 1996 +0100
@@ -100,6 +100,8 @@
   Inter         :: (('a set) set) => 'a set           ("\\<Inter> _" [90] 90)
   "@Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
   "@Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
+
+syntax (symbols output)
   "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
   "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)