--- 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)
+
--- 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)