| changeset 467 | 92868dab2939 |
| parent 437 | 435875e4b21d |
| child 484 | 70b789956bd3 |
--- a/src/ZF/Cardinal.ML Tue Jul 12 14:26:04 1994 +0200 +++ b/src/ZF/Cardinal.ML Tue Jul 12 18:05:03 1994 +0200 @@ -181,7 +181,7 @@ by (rtac LeastI 1); by (etac Ord_ordertype 2); by (rtac exI 1); -by (etac (ordertype_bij RS bij_converse_bij) 1); +by (etac (ordermap_bij RS bij_converse_bij) 1); val well_ord_cardinal_eqpoll = result(); val Ord_cardinal_eqpoll = well_ord_Memrel RS well_ord_cardinal_eqpoll