| changeset 3887 | 04f730731e43 |
| parent 3840 | e0baea4d485a |
| child 4091 | 771b1f6422a8 |
--- a/src/ZF/CardinalArith.ML Thu Oct 16 13:36:04 1997 +0200 +++ b/src/ZF/CardinalArith.ML Thu Oct 16 13:38:28 1997 +0200 @@ -798,7 +798,8 @@ (** Thanks to Krzysztof Grabczewski **) -val nat_implies_well_ord = nat_into_Ord RS well_ord_Memrel; +val nat_implies_well_ord = + (transfer CardinalArith.thy nat_into_Ord) RS well_ord_Memrel; goal CardinalArith.thy "!!m n. [| m:nat; n:nat |] ==> m + n eqpoll m #+ n"; by (rtac eqpoll_trans 1);