# HG changeset patch
# User wenzelm
# Date 850227233 -3600
# Node ID a2999e19703ba08a1c886c4860a9fd0f5f635e58
# Parent  c5dc6f8b385b2928424be8ea90f66b92da57ac47
fixed alternative quantifier symbol syntax;

diff -r c5dc6f8b385b -r a2999e19703b src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Dec 10 15:08:57 1996 +0100
+++ b/src/HOL/HOL.thy	Tue Dec 10 15:13:53 1996 +0100
@@ -123,10 +123,13 @@
   "! "          :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
   "? "          :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
   "?! "         :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
+  "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<mapsto>/ _)" 10)
+
+syntax (symbols output)
   "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
   "*Ex"         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
   "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
-  "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<mapsto>/ _)" 10)
+
 
 
 
diff -r c5dc6f8b385b -r a2999e19703b src/HOL/Set.thy
--- 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)