equal
deleted
inserted
replaced
796 qed "Finite_imp_cardinal_Diff"; |
796 qed "Finite_imp_cardinal_Diff"; |
797 |
797 |
798 |
798 |
799 (** Thanks to Krzysztof Grabczewski **) |
799 (** Thanks to Krzysztof Grabczewski **) |
800 |
800 |
801 val nat_implies_well_ord = nat_into_Ord RS well_ord_Memrel; |
801 val nat_implies_well_ord = |
|
802 (transfer CardinalArith.thy nat_into_Ord) RS well_ord_Memrel; |
802 |
803 |
803 goal CardinalArith.thy "!!m n. [| m:nat; n:nat |] ==> m + n eqpoll m #+ n"; |
804 goal CardinalArith.thy "!!m n. [| m:nat; n:nat |] ==> m + n eqpoll m #+ n"; |
804 by (rtac eqpoll_trans 1); |
805 by (rtac eqpoll_trans 1); |
805 by (eresolve_tac [nat_implies_well_ord RS ( |
806 by (eresolve_tac [nat_implies_well_ord RS ( |
806 nat_implies_well_ord RSN (2, |
807 nat_implies_well_ord RSN (2, |