--- a/HOL.thy Mon Dec 13 18:43:03 1993 +0100
+++ b/HOL.thy Tue Dec 14 18:05:22 1993 +0100
@@ -19,6 +19,7 @@
types
bool 0
+ letbinds, letbind 0
arities
fun :: (term, term) term
@@ -43,7 +44,10 @@
Ex1 :: "('a => bool) => bool" (binder "?! " 10)
Let :: "['a, 'a => 'b] => 'b"
- "@Let" :: "[idt, 'a, 'b] => 'b" ("(let _ = (2_)/ in (2_))" 10)
+ "_bind" :: "[idt, 'a] => letbind" ("(2_ =/ _)" 10)
+ "" :: "letbind => letbinds" ("_")
+ "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _")
+ "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10)
(* Alternative Quantifiers *)
@@ -72,8 +76,8 @@
"EX xs. P" => "? xs. P"
"EX! xs. P" => "?! xs. P"
"x ~= y" == "~ (x = y)"
- "let x = s in t" == "Let(s, %x. t)"
-
+ "_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))"
+ "let x = a in e" == "Let(a, %x. e)"
rules