src/ZF/AC/AC16_WO4.thy
changeset 58860 fee7cfa69c50
parent 46822 95f1e700b712
child 59788 6f7b6adac439
     1.1 --- a/src/ZF/AC/AC16_WO4.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/ZF/AC/AC16_WO4.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4  (* There exists a well ordered set y such that ...                        *)
     1.5  (* ********************************************************************** *)
     1.6  
     1.7 -lemmas lepoll_paired = paired_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll];
     1.8 +lemmas lepoll_paired = paired_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll]
     1.9  
    1.10  lemma lemma2: "\<exists>y R. well_ord(y,R) & x \<inter> y = 0 & ~y \<lesssim> z & ~Finite(y)"
    1.11  apply (rule_tac x = "{{a,x}. a \<in> nat \<union> Hartog (z) }" in exI)