src/ZF/Constructible/AC_in_L.thy

--- a/src/ZF/Constructible/AC_in_L.thy	Wed Aug 27 18:22:34 2003 +0200
+++ b/src/ZF/Constructible/AC_in_L.thy	Thu Aug 28 01:56:40 2003 +0200
@@ -244,7 +244,7 @@
 
   DPow_least :: "[i,i,i,i]=>i"
     --{*function yielding the smallest index for @{term X}*}
-   "DPow_least(f,r,A,X) == \<mu>k. DPow_ord(f,r,A,X,k)"
+   "DPow_least(f,r,A,X) == \<mu> k. DPow_ord(f,r,A,X,k)"
 
   DPow_r :: "[i,i,i]=>i"
     --{*a wellordering on @{term "DPow(A)"}*}