fixed pris of binder syntax;
authorwenzelm
Tue Dec 10 14:09:32 1996 +0100 (1996-12-10)
changeset 2368d394336997cf
parent 2367 eba760ebe315
child 2369 8100f00e8950
fixed pris of binder syntax;
src/HOL/HOL.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/HOL.thy	Tue Dec 10 13:03:44 1996 +0100
     1.2 +++ b/src/HOL/HOL.thy	Tue Dec 10 14:09:32 1996 +0100
     1.3 @@ -80,13 +80,13 @@
     1.4  
     1.5    "~="          :: ['a, 'a] => bool                 (infixl 50)
     1.6  
     1.7 -  "@Eps"        :: [pttrn, bool] => 'a              ("(3@ _./ _)" 10)
     1.8 +  "@Eps"        :: [pttrn, bool] => 'a              ("(3@ _./ _)" [0, 10] 10)
     1.9  
    1.10    (* Alternative Quantifiers *)
    1.11  
    1.12 -  "*All"        :: [idts, bool] => bool             ("(3ALL _./ _)" 10)
    1.13 -  "*Ex"         :: [idts, bool] => bool             ("(3EX _./ _)" 10)
    1.14 -  "*Ex1"        :: [idts, bool] => bool             ("(3EX! _./ _)" 10)
    1.15 +  "*All"        :: [idts, bool] => bool             ("(3ALL _./ _)" [0, 10] 10)
    1.16 +  "*Ex"         :: [idts, bool] => bool             ("(3EX _./ _)" [0, 10] 10)
    1.17 +  "*Ex1"        :: [idts, bool] => bool             ("(3EX! _./ _)" [0, 10] 10)
    1.18  
    1.19    (* Let expressions *)
    1.20  
    1.21 @@ -119,13 +119,13 @@
    1.22    "op -->"      :: [bool, bool] => bool             (infixr "\\<midarrow>\\<rightarrow>" 25)
    1.23    "op o"        :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl "\\<circ>" 55)
    1.24    "op ~="       :: ['a, 'a] => bool                 (infixl "\\<noteq>" 50)
    1.25 -  "@Eps"        :: [pttrn, bool] => 'a              ("(3\\<epsilon>_./ _)" 10)
    1.26 -  "! "          :: [idts, bool] => bool             ("(3\\<forall>_./ _)" 10)
    1.27 -  "? "          :: [idts, bool] => bool             ("(3\\<exists>_./ _)" 10)
    1.28 -  "?! "         :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" 10)
    1.29 -  "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" 10)
    1.30 -  "*Ex"         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" 10)
    1.31 -  "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" 10)
    1.32 +  "@Eps"        :: [pttrn, bool] => 'a              ("(3\\<epsilon>_./ _)" [0, 10] 10)
    1.33 +  "! "          :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
    1.34 +  "? "          :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
    1.35 +  "?! "         :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
    1.36 +  "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
    1.37 +  "*Ex"         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
    1.38 +  "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
    1.39    "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<mapsto>/ _)" 10)
    1.40  
    1.41  
     2.1 --- a/src/HOL/Set.thy	Tue Dec 10 13:03:44 1996 +0100
     2.2 +++ b/src/HOL/Set.thy	Tue Dec 10 14:09:32 1996 +0100
     2.3 @@ -65,10 +65,10 @@
     2.4  
     2.5    (* Bounded Quantifiers *)
     2.6  
     2.7 -  "@Ball"       :: [pttrn, 'a set, bool] => bool      ("(3! _:_./ _)" 10)
     2.8 -  "@Bex"        :: [pttrn, 'a set, bool] => bool      ("(3? _:_./ _)" 10)
     2.9 -  "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3ALL _:_./ _)" 10)
    2.10 -  "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3EX _:_./ _)" 10)
    2.11 +  "@Ball"       :: [pttrn, 'a set, bool] => bool      ("(3! _:_./ _)" [0, 0, 10] 10)
    2.12 +  "@Bex"        :: [pttrn, 'a set, bool] => bool      ("(3? _:_./ _)" [0, 0, 10] 10)
    2.13 +  "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3ALL _:_./ _)" [0, 0, 10] 10)
    2.14 +  "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3EX _:_./ _)" [0, 0, 10] 10)
    2.15  
    2.16  translations
    2.17    "UNIV"        == "Compl {}"
    2.18 @@ -98,10 +98,10 @@
    2.19    "@INTER"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Inter> _\\<in>_./ _)" 10)
    2.20    Union         :: (('a set) set) => 'a set           ("\\<Union> _" [90] 90)
    2.21    Inter         :: (('a set) set) => 'a set           ("\\<Inter> _" [90] 90)
    2.22 -  "@Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" 10)
    2.23 -  "@Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" 10)
    2.24 -  "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" 10)
    2.25 -  "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" 10)
    2.26 +  "@Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
    2.27 +  "@Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
    2.28 +  "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
    2.29 +  "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
    2.30  
    2.31  
    2.32