src/HOL/Finite.ML
changeset 5278 a903b66822e2
parent 5183 89f162de39cf
child 5316 7a8975451a89
     1.1 --- a/src/HOL/Finite.ML	Thu Aug 06 15:47:26 1998 +0200
     1.2 +++ b/src/HOL/Finite.ML	Thu Aug 06 15:48:13 1998 +0200
     1.3 @@ -211,9 +211,8 @@
     1.4                            addcongs [rev_conj_cong]) 1);
     1.5  qed "finite_has_card";
     1.6  
     1.7 -Goal
     1.8 -  "[| x ~: A; insert x A = {f i|i. i<n} |] ==> \
     1.9 -\  ? m::nat. m<n & (? g. A = {g i|i. i<m})";
    1.10 +Goal "[| x ~: A; insert x A = {f i|i. i<n} |]  \
    1.11 +\     ==> ? m::nat. m<n & (? g. A = {g i|i. i<m})";
    1.12  by (exhaust_tac "n" 1);
    1.13   by (hyp_subst_tac 1);
    1.14   by (Asm_full_simp_tac 1);