--- a/src/HOL/HOL.thy Tue Apr 29 17:23:53 1997 +0200
+++ b/src/HOL/HOL.thy Tue Apr 29 17:38:02 1997 +0200
@@ -123,7 +123,7 @@
"? " :: [idts, bool] => bool ("(3\\<exists>_./ _)" [0, 10] 10)
"?! " :: [idts, bool] => bool ("(3\\<exists>!_./ _)" [0, 10] 10)
"@case1" :: ['a, 'b] => case_syn ("(2_ \\<Rightarrow>/ _)" 10)
- "@case2" :: [case_syn, cases_syn] => cases_syn ("_/ \\<orelse> _")
+(*"@case2" :: [case_syn, cases_syn] => cases_syn ("_/ \\<orelse> _")*)
syntax (symbols output)
"*All" :: [idts, bool] => bool ("(3\\<forall>_./ _)" [0, 10] 10)