--- a/src/HOL/Set.thy Tue Dec 10 13:03:44 1996 +0100
+++ b/src/HOL/Set.thy Tue Dec 10 14:09:32 1996 +0100
@@ -65,10 +65,10 @@
(* Bounded Quantifiers *)
- "@Ball" :: [pttrn, 'a set, bool] => bool ("(3! _:_./ _)" 10)
- "@Bex" :: [pttrn, 'a set, bool] => bool ("(3? _:_./ _)" 10)
- "*Ball" :: [pttrn, 'a set, bool] => bool ("(3ALL _:_./ _)" 10)
- "*Bex" :: [pttrn, 'a set, bool] => bool ("(3EX _:_./ _)" 10)
+ "@Ball" :: [pttrn, 'a set, bool] => bool ("(3! _:_./ _)" [0, 0, 10] 10)
+ "@Bex" :: [pttrn, 'a set, bool] => bool ("(3? _:_./ _)" [0, 0, 10] 10)
+ "*Ball" :: [pttrn, 'a set, bool] => bool ("(3ALL _:_./ _)" [0, 0, 10] 10)
+ "*Bex" :: [pttrn, 'a set, bool] => bool ("(3EX _:_./ _)" [0, 0, 10] 10)
translations
"UNIV" == "Compl {}"
@@ -98,10 +98,10 @@
"@INTER" :: [pttrn, 'a set, 'b set] => 'b set ("(3\\<Inter> _\\<in>_./ _)" 10)
Union :: (('a set) set) => 'a set ("\\<Union> _" [90] 90)
Inter :: (('a set) set) => 'a set ("\\<Inter> _" [90] 90)
- "@Ball" :: [pttrn, 'a set, bool] => bool ("(3\\<forall> _\\<in>_./ _)" 10)
- "@Bex" :: [pttrn, 'a set, bool] => bool ("(3\\<exists> _\\<in>_./ _)" 10)
- "*Ball" :: [pttrn, 'a set, bool] => bool ("(3\\<forall> _\\<in>_./ _)" 10)
- "*Bex" :: [pttrn, 'a set, bool] => bool ("(3\\<exists> _\\<in>_./ _)" 10)
+ "@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)
+ "*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)