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