--- 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)