src/HOL/HOL.thy
changeset 3066 3c548f92e032
parent 2912 3fac3e8d5d3e
child 3068 b7562e452816
     1.1 --- a/src/HOL/HOL.thy	Tue Apr 29 17:13:41 1997 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Apr 29 17:14:06 1997 +0200
     1.3 @@ -123,6 +123,7 @@
     1.4    "? "          :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
     1.5    "?! "         :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
     1.6    "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<Rightarrow>/ _)" 10)
     1.7 +  "@case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ \\<orelse> _")
     1.8  
     1.9  syntax (symbols output)
    1.10    "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)