changeset 5147 | 825877190618 |
parent 5068 | fb28eaa07e01 |
child 5241 | e5129172cb2b |
--- a/src/ZF/AC/AC1_WO2.ML Wed Jul 15 12:02:19 1998 +0200 +++ b/src/ZF/AC/AC1_WO2.ML Wed Jul 15 14:13:18 1998 +0200 @@ -17,7 +17,7 @@ by (fast_tac (claset() addSIs [prem RS Pi_weaken_type]) 1); val lemma1 = uresult() |> standard; -Goalw [AC1_def, WO2_def, eqpoll_def] "!!Z. AC1 ==> WO2"; +Goalw [AC1_def, WO2_def, eqpoll_def] "AC1 ==> WO2"; by (rtac allI 1); by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1); by (fast_tac (claset() addSDs [lemma1] addSIs [Ord_Least]) 1);