changeset 45602 | 2a858377c3d2 |
parent 32960 | 69916a850301 |
child 46954 | d8b3412cdb99 |
--- a/src/ZF/AC/HH.thy Sun Nov 20 17:57:09 2011 +0100 +++ b/src/ZF/AC/HH.thy Sun Nov 20 20:15:02 2011 +0100 @@ -210,7 +210,7 @@ simplification is needed!*) lemmas bij_Least_HH_x = comp_bij [OF f_sing_lam_bij [OF _ lam_singI] - lam_sing_bij [THEN bij_converse_bij], standard] + lam_sing_bij [THEN bij_converse_bij]] subsection{*The proof of AC1 ==> WO2*}