src/ZF/Finite.ML
changeset 9211 6236c5285bd8
parent 9173 422968aeed49
child 9907 473a6604da94
     1.1 --- a/src/ZF/Finite.ML	Fri Jun 30 12:49:11 2000 +0200
     1.2 +++ b/src/ZF/Finite.ML	Fri Jun 30 12:51:30 2000 +0200
     1.3 @@ -48,8 +48,8 @@
     1.4  
     1.5  
     1.6  (*The union of a set of finite sets is finite.*)
     1.7 -val [major] = goal Finite.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)";
     1.8 -by (rtac (major RS Fin_induct) 1);
     1.9 +Goal "C : Fin(Fin(A)) ==> Union(C) : Fin(A)";
    1.10 +by (etac Fin_induct 1);
    1.11  by (ALLGOALS Asm_simp_tac);
    1.12  qed "Fin_UnionI";
    1.13