# HG changeset patch
# User lcp
# Date 799504071 -7200
# Node ID 840554ac04512e1e9f72b9c10a8de42053beadb3
# Parent  c2b3b7b7a69fd4952d8ccc4e152aca3003147155
Patterns can now be let-bound

diff -r c2b3b7b7a69f -r 840554ac0451 src/ZF/Let.thy
--- a/src/ZF/Let.thy	Wed May 03 14:17:01 1995 +0200
+++ b/src/ZF/Let.thy	Wed May 03 14:27:51 1995 +0200
@@ -3,10 +3,10 @@
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 
-Let expressions -- borrowed from HOL
+Let expressions, and tuple pattern-matching (borrowed from HOL)
 *)
 
-Let = ZF +
+Let = FOL +
 
 types
   letbinds  letbind
@@ -15,7 +15,7 @@
   Let           :: "['a, 'a => 'b] => 'b"
 
 syntax
-  "_bind"       :: "[idt, 'a] => letbind"             ("(2_ =/ _)" 10)
+  "_bind"       :: "[pttrn, 'a] => letbind"           ("(2_ =/ _)" 10)
   ""            :: "letbind => letbinds"              ("_")
   "_binds"      :: "[letbind, letbinds] => letbinds"  ("_;/ _")
   "_Let"        :: "[letbinds, 'a] => 'a"             ("(let (_)/ in (_))" 10)