changeset 5315 | c9ad6bbf3a34 |
parent 5268 | 59ef39008514 |
child 6068 | 2d8f3e1f1151 |
--- a/src/ZF/AC/WO2_AC16.ML Thu Aug 13 18:07:38 1998 +0200 +++ b/src/ZF/AC/WO2_AC16.ML Thu Aug 13 18:07:56 1998 +0200 @@ -601,8 +601,7 @@ (* ********************************************************************** *) -Goalw [AC16_def] - "!!n k. [| WO2; 0<m; k:nat; m:nat |] ==> AC16(k #+ m,k)"; +Goalw [AC16_def] "[| WO2; 0<m; k:nat; m:nat |] ==> AC16(k #+ m,k)"; by (rtac allI 1); by (rtac impI 1); by (forward_tac [WO2_infinite_subsets_eqpoll_X] 1