diff -r 65a546c2b8ed -r 7ef6ba42914b hol.thy
--- a/hol.thy	Mon Jan 24 16:03:03 1994 +0100
+++ b/hol.thy	Wed Jan 26 17:53:27 1994 +0100
@@ -20,6 +20,7 @@
 types
   bool 0
   letbinds, letbind 0
+  case_syn,cases_syn 0
 
 arities
   fun :: (term, term) term
@@ -49,6 +50,13 @@
   "_binds"      :: "[letbind, letbinds] => letbinds"  ("_;/ _")
   "_Let"        :: "[letbinds, 'a] => 'a"            ("(let (_)/ in (_))" 10)
 
+  (* Case expressions *)
+
+  "@case"            :: "['a, cases_syn] => 'b"		("(case _ of/ _)" 10)
+  "@case1"           :: "['a, 'b] => case_syn"		("(2_ =>/ _)" 10)
+  ""                 :: "case_syn => cases_syn"		("_")
+  "@case2"           :: "[case_syn,cases_syn] => cases_syn"	("_/ | _")
+
   (* Alternative Quantifiers *)
 
   "*All"        :: "[idts, bool] => bool"             ("(3ALL _./ _)" 10)