--- a/src/HOL/HOL.thy Tue Dec 10 13:03:44 1996 +0100
+++ b/src/HOL/HOL.thy Tue Dec 10 14:09:32 1996 +0100
@@ -80,13 +80,13 @@
"~=" :: ['a, 'a] => bool (infixl 50)
- "@Eps" :: [pttrn, bool] => 'a ("(3@ _./ _)" 10)
+ "@Eps" :: [pttrn, bool] => 'a ("(3@ _./ _)" [0, 10] 10)
(* Alternative Quantifiers *)
- "*All" :: [idts, bool] => bool ("(3ALL _./ _)" 10)
- "*Ex" :: [idts, bool] => bool ("(3EX _./ _)" 10)
- "*Ex1" :: [idts, bool] => bool ("(3EX! _./ _)" 10)
+ "*All" :: [idts, bool] => bool ("(3ALL _./ _)" [0, 10] 10)
+ "*Ex" :: [idts, bool] => bool ("(3EX _./ _)" [0, 10] 10)
+ "*Ex1" :: [idts, bool] => bool ("(3EX! _./ _)" [0, 10] 10)
(* Let expressions *)
@@ -119,13 +119,13 @@
"op -->" :: [bool, bool] => bool (infixr "\\<midarrow>\\<rightarrow>" 25)
"op o" :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl "\\<circ>" 55)
"op ~=" :: ['a, 'a] => bool (infixl "\\<noteq>" 50)
- "@Eps" :: [pttrn, bool] => 'a ("(3\\<epsilon>_./ _)" 10)
- "! " :: [idts, bool] => bool ("(3\\<forall>_./ _)" 10)
- "? " :: [idts, bool] => bool ("(3\\<exists>_./ _)" 10)
- "?! " :: [idts, bool] => bool ("(3\\<exists>!_./ _)" 10)
- "*All" :: [idts, bool] => bool ("(3\\<forall>_./ _)" 10)
- "*Ex" :: [idts, bool] => bool ("(3\\<exists>_./ _)" 10)
- "*Ex1" :: [idts, bool] => bool ("(3\\<exists>!_./ _)" 10)
+ "@Eps" :: [pttrn, bool] => 'a ("(3\\<epsilon>_./ _)" [0, 10] 10)
+ "! " :: [idts, bool] => bool ("(3\\<forall>_./ _)" [0, 10] 10)
+ "? " :: [idts, bool] => bool ("(3\\<exists>_./ _)" [0, 10] 10)
+ "?! " :: [idts, bool] => bool ("(3\\<exists>!_./ _)" [0, 10] 10)
+ "*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 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)