src/ZF/AC/AC1_WO2.ML
changeset 5147 825877190618
parent 5068 fb28eaa07e01
child 5241 e5129172cb2b
equal deleted inserted replaced
5146:1ea751ae62b2 5147:825877190618
    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 [AC1_def, WO2_def, eqpoll_def] "!!Z. AC1 ==> WO2";
    20 Goalw [AC1_def, WO2_def, eqpoll_def] "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";