fixed alternative quantifier symbol syntax;
authorwenzelm
Tue Dec 10 15:13:53 1996 +0100 (1996-12-10)
changeset 2372a2999e19703b
parent 2371 c5dc6f8b385b
child 2373 490ffa16952e
fixed alternative quantifier symbol syntax;
src/HOL/HOL.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/HOL.thy	Tue Dec 10 15:08:57 1996 +0100
     1.2 +++ b/src/HOL/HOL.thy	Tue Dec 10 15:13:53 1996 +0100
     1.3 @@ -123,10 +123,13 @@
     1.4    "! "          :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
     1.5    "? "          :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
     1.6    "?! "         :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
     1.7 +  "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<mapsto>/ _)" 10)
     1.8 +
     1.9 +syntax (symbols output)
    1.10    "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
    1.11    "*Ex"         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
    1.12    "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
    1.13 -  "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<mapsto>/ _)" 10)
    1.14 +
    1.15  
    1.16  
    1.17  
     2.1 --- a/src/HOL/Set.thy	Tue Dec 10 15:08:57 1996 +0100
     2.2 +++ b/src/HOL/Set.thy	Tue Dec 10 15:13:53 1996 +0100
     2.3 @@ -100,6 +100,8 @@
     2.4    Inter         :: (('a set) set) => 'a set           ("\\<Inter> _" [90] 90)
     2.5    "@Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
     2.6    "@Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
     2.7 +
     2.8 +syntax (symbols output)
     2.9    "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3\\<forall> _\\<in>_./ _)" [0, 0, 10] 10)
    2.10    "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3\\<exists> _\\<in>_./ _)" [0, 0, 10] 10)
    2.11