src/ZF/Constructible/AC_in_L.thy
changeset 14171 0cab06e3bbd0
parent 13702 c7cf8fa66534
child 16417 9bc16273c2d4
     1.1 --- a/src/ZF/Constructible/AC_in_L.thy	Wed Aug 27 18:22:34 2003 +0200
     1.2 +++ b/src/ZF/Constructible/AC_in_L.thy	Thu Aug 28 01:56:40 2003 +0200
     1.3 @@ -244,7 +244,7 @@
     1.4  
     1.5    DPow_least :: "[i,i,i,i]=>i"
     1.6      --{*function yielding the smallest index for @{term X}*}
     1.7 -   "DPow_least(f,r,A,X) == \<mu>k. DPow_ord(f,r,A,X,k)"
     1.8 +   "DPow_least(f,r,A,X) == \<mu> k. DPow_ord(f,r,A,X,k)"
     1.9  
    1.10    DPow_r :: "[i,i,i]=>i"
    1.11      --{*a wellordering on @{term "DPow(A)"}*}