equal
deleted
inserted
replaced
15 by (resolve_tac [lam_type RS apply_type] 1 THEN (assume_tac 2)); |
15 by (resolve_tac [lam_type RS apply_type] 1 THEN (assume_tac 2)); |
16 by (fast_tac (claset() addSDs [equals0D, prem RS apply_type]) 1); |
16 by (fast_tac (claset() addSDs [equals0D, prem RS apply_type]) 1); |
17 by (fast_tac (claset() addSIs [prem RS Pi_weaken_type]) 1); |
17 by (fast_tac (claset() addSIs [prem RS Pi_weaken_type]) 1); |
18 val lemma1 = uresult() |> standard; |
18 val lemma1 = uresult() |> standard; |
19 |
19 |
20 goalw thy [AC1_def, WO2_def, eqpoll_def] "!!Z. AC1 ==> WO2"; |
20 Goalw [AC1_def, WO2_def, eqpoll_def] "!!Z. AC1 ==> WO2"; |
21 by (rtac allI 1); |
21 by (rtac allI 1); |
22 by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1); |
22 by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1); |
23 by (fast_tac (claset() addSDs [lemma1] addSIs [Ord_Least]) 1); |
23 by (fast_tac (claset() addSDs [lemma1] addSIs [Ord_Least]) 1); |
24 qed "AC1_WO2"; |
24 qed "AC1_WO2"; |