src/ZF/CardinalArith.thy
changeset 13269 3ba9be497c33
parent 13244 7b37e218f298
child 13328 703de709a64b
     1.1 --- a/src/ZF/CardinalArith.thy	Mon Jul 01 18:16:18 2002 +0200
     1.2 +++ b/src/ZF/CardinalArith.thy	Tue Jul 02 13:28:08 2002 +0200
     1.3 @@ -467,7 +467,7 @@
     1.4  
     1.5  (*A general fact about ordermap*)
     1.6  lemma ordermap_eqpoll_pred:
     1.7 -    "[| well_ord(A,r);  x:A |] ==> ordermap(A,r)`x \<approx> pred(A,x,r)"
     1.8 +    "[| well_ord(A,r);  x:A |] ==> ordermap(A,r)`x \<approx> Order.pred(A,x,r)"
     1.9  apply (unfold eqpoll_def)
    1.10  apply (rule exI)
    1.11  apply (simp add: ordermap_eq_image well_ord_is_wf)
    1.12 @@ -503,7 +503,7 @@
    1.13  done
    1.14  
    1.15  lemma pred_csquare_subset: 
    1.16 -    "z<K ==> pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)"
    1.17 +    "z<K ==> Order.pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)"
    1.18  apply (unfold Order.pred_def)
    1.19  apply (safe del: SigmaI succCI)
    1.20  apply (erule csquareD [THEN conjE])