# HG changeset patch
# User paulson
# Date 894014584 -7200
# Node ID 58656c6a3551680fb63f46ad36c91899885e2105
# Parent  96578989b0d65287a12771ac7af7fa93998be1d1
"let" is no longer restricted to FOL terms and allows any logical terms

diff -r 96578989b0d6 -r 58656c6a3551 NEWS
--- a/NEWS	Fri May 01 11:22:09 1998 +0200
+++ b/NEWS	Fri May 01 11:23:04 1998 +0200
@@ -96,6 +96,9 @@
 
 * many new identities for unions, intersections, set difference, etc.;
 
+*** ZF ***
+
+* in  let x=t in u(x), neither t nor u(x) has to be an FOL term.
 
 
 New in Isabelle98 (January 1998)
diff -r 96578989b0d6 -r 58656c6a3551 src/ZF/Let.thy
--- a/src/ZF/Let.thy	Fri May 01 11:22:09 1998 +0200
+++ b/src/ZF/Let.thy	Fri May 01 11:23:04 1998 +0200
@@ -12,7 +12,7 @@
   letbinds  letbind
 
 consts
-  Let           :: ['a, 'a => 'b] => 'b
+  Let           :: ['a::logic, 'a => 'b] => ('b::logic)
 
 syntax
   "_bind"       :: [pttrn, 'a] => letbind           ("(2_ =/ _)" 10)