# HG changeset patch
# User nipkow
# Date 755888722 -3600
# Node ID 5d95fe89f501a9a2afcb497ee518542577c1b92f
# Parent  340d21c86440cf9cb3a7158955daf72ae069f3a1
added syntax for nested lets.

diff -r 340d21c86440 -r 5d95fe89f501 HOL.thy
--- 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
 
diff -r 340d21c86440 -r 5d95fe89f501 hol.thy
--- 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