changeset 3066 | 3c548f92e032 |
parent 2912 | 3fac3e8d5d3e |
child 3068 | b7562e452816 |
--- 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\\<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> _") syntax (symbols output) "*All" :: [idts, bool] => bool ("(3\\<forall>_./ _)" [0, 10] 10)