src/ZF/AC/HH.thy

--- a/src/ZF/AC/HH.thy	Tue Jul 25 17:03:59 1995 +0200
+++ b/src/ZF/AC/HH.thy	Tue Jul 25 17:31:53 1995 +0200
@@ -8,7 +8,7 @@
   AC15 ==> WO6
 *)
 
-HH = AC_Equiv + Hartog + WO_AC +
+HH = AC_Equiv + Hartog + WO_AC + Let +
 
 consts
  
@@ -16,8 +16,8 @@
 
 defs
 
-  HH_def  "HH(f,x,a)  == transrec(a, %b r. (lam z:Pow(x).   
-	                 if(f`z:Pow(z)-{0}, f`z, {x}))`(x - (UN c:b. r`c)))"
+  HH_def  "HH(f,x,a) == transrec(a, %b r. let z = x - (UN c:b. r`c)
+                        in  if(f`z:Pow(z)-{0}, f`z, {x}))"
 
 end