diff -r c57861f709d2 -r 3c548f92e032 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Tue Apr 29 17:13:41 1997 +0200 +++ b/src/HOL/HOL.thy Tue Apr 29 17:14:06 1997 +0200 @@ -123,6 +123,7 @@ "? " :: [idts, bool] => bool ("(3\\_./ _)" [0, 10] 10) "?! " :: [idts, bool] => bool ("(3\\!_./ _)" [0, 10] 10) "@case1" :: ['a, 'b] => case_syn ("(2_ \\/ _)" 10) + "@case2" :: [case_syn, cases_syn] => cases_syn ("_/ \\ _") syntax (symbols output) "*All" :: [idts, bool] => bool ("(3\\_./ _)" [0, 10] 10)