src/HOL/HOL.thy
changeset 2372 a2999e19703b
parent 2368 d394336997cf
child 2393 651fce76c86c
     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