equal
deleted
inserted
replaced
17 by (Fast_tac 1); |
17 by (Fast_tac 1); |
18 qed "WO2_WO3"; |
18 qed "WO2_WO3"; |
19 |
19 |
20 (* ********************************************************************** *) |
20 (* ********************************************************************** *) |
21 |
21 |
22 Goalw (eqpoll_def::WO_defs) "!!Z. WO3 ==> WO1"; |
22 Goalw (eqpoll_def::WO_defs) "WO3 ==> WO1"; |
23 by (fast_tac (claset() addSEs [bij_is_inj RS well_ord_rvimage, |
23 by (fast_tac (claset() addSEs [bij_is_inj RS well_ord_rvimage, |
24 well_ord_Memrel RS well_ord_subset]) 1); |
24 well_ord_Memrel RS well_ord_subset]) 1); |
25 qed "WO3_WO1"; |
25 qed "WO3_WO1"; |
26 |
26 |
27 (* ********************************************************************** *) |
27 (* ********************************************************************** *) |
28 |
28 |
29 Goalw (eqpoll_def::WO_defs) "!!Z. WO1 ==> WO2"; |
29 Goalw (eqpoll_def::WO_defs) "WO1 ==> WO2"; |
30 by (fast_tac (claset() addSIs [Ord_ordertype, ordermap_bij]) 1); |
30 by (fast_tac (claset() addSIs [Ord_ordertype, ordermap_bij]) 1); |
31 qed "WO1_WO2"; |
31 qed "WO1_WO2"; |
32 |
32 |
33 (* ********************************************************************** *) |
33 (* ********************************************************************** *) |
34 |
34 |