1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Sat Nov 27 17:44:36 2010 -0800
     1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Sun Nov 28 15:20:51 2010 +0100
     1.3 @@ -130,7 +130,7 @@
     1.4     apply (rule Suc_le_mono [THEN subst])
     1.5     apply (simp add: card_Suc_Diff1)
     1.6    apply (rule_tac A1 = "Aa - {xb}" in finite_imp_foldSetD [THEN exE])
     1.7 -     apply (blast intro: foldSetD_imp_finite finite_Diff)
     1.8 +     apply (blast intro: foldSetD_imp_finite)
     1.9      apply best
    1.10     apply assumption
    1.11    apply (frule (1) Diff1_foldSetD)

     2.1 --- a/src/HOL/Big_Operators.thy	Sat Nov 27 17:44:36 2010 -0800
     2.2 +++ b/src/HOL/Big_Operators.thy	Sun Nov 28 15:20:51 2010 +0100
     2.3 @@ -707,7 +707,7 @@
     2.4  proof -
     2.5    have "A <+> B = Inl ` A \<union> Inr ` B" by auto
     2.6    moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)"
     2.7 -    by(auto intro: finite_imageI)
     2.8 +    by auto
     2.9    moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto
    2.10    moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI)
    2.11    ultimately show ?thesis using fin by(simp add: setsum_Un_disjoint setsum_reindex)

     3.1 --- a/src/HOL/Finite_Set.thy	Sat Nov 27 17:44:36 2010 -0800
     3.2 +++ b/src/HOL/Finite_Set.thy	Sun Nov 28 15:20:51 2010 +0100
     3.3 @@ -274,7 +274,7 @@
     3.4    then show ?thesis by simp
     3.5  qed
     3.6  
     3.7 -lemma finite_Diff [simp]: "finite A ==> finite (A - B)"
     3.8 +lemma finite_Diff [simp, intro]: "finite A ==> finite (A - B)"
     3.9  by (rule Diff_subset [THEN finite_subset])
    3.10  
    3.11  lemma finite_Diff2 [simp]:
    3.12 @@ -303,7 +303,7 @@
    3.13  
    3.14  text {* Image and Inverse Image over Finite Sets *}
    3.15  
    3.16 -lemma finite_imageI[simp]: "finite F ==> finite (h ` F)"
    3.17 +lemma finite_imageI[simp, intro]: "finite F ==> finite (h ` F)"
    3.18    -- {* The image of a finite set is finite. *}
    3.19    by (induct set: finite) simp_all
    3.20  
    3.21 @@ -372,8 +372,9 @@
    3.22  
    3.23  text {* The finite UNION of finite sets *}
    3.24  
    3.25 -lemma finite_UN_I: "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
    3.26 -  by (induct set: finite) simp_all
    3.27 +lemma finite_UN_I[intro]:
    3.28 +  "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (UN a:A. B a)"
    3.29 +by (induct set: finite) simp_all
    3.30  
    3.31  text {*
    3.32    Strengthen RHS to
    3.33 @@ -385,7 +386,7 @@
    3.34  
    3.35  lemma finite_UN [simp]:
    3.36    "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
    3.37 -by (blast intro: finite_UN_I finite_subset)
    3.38 +by (blast intro: finite_subset)
    3.39  
    3.40  lemma finite_Collect_bex[simp]: "finite A \<Longrightarrow>
    3.41    finite{x. EX y:A. Q x y} = (ALL y:A. finite{x. Q x y})"
    3.42 @@ -428,9 +429,9 @@
    3.43  
    3.44  text {* Sigma of finite sets *}
    3.45  
    3.46 -lemma finite_SigmaI [simp]:
    3.47 +lemma finite_SigmaI [simp, intro]:
    3.48      "finite A ==> (!!a. a:A ==> finite (B a)) ==> finite (SIGMA a:A. B a)"
    3.49 -  by (unfold Sigma_def) (blast intro!: finite_UN_I)
    3.50 +  by (unfold Sigma_def) blast
    3.51  
    3.52  lemma finite_cartesian_product: "[| finite A; finite B |] ==>
    3.53      finite (A <*> B)"
    3.54 @@ -2266,7 +2267,7 @@
    3.55  apply (induct set: finite)
    3.56   apply (simp_all add: Pow_insert)
    3.57  apply (subst card_Un_disjoint, blast)
    3.58 -  apply (blast intro: finite_imageI, blast)
    3.59 +  apply (blast, blast)
    3.60  apply (subgoal_tac "inj_on (insert x) (Pow F)")
    3.61   apply (simp add: card_image Pow_insert)
    3.62  apply (unfold inj_on_def)

     4.1 --- a/src/HOL/IMPP/Hoare.thy	Sat Nov 27 17:44:36 2010 -0800
     4.2 +++ b/src/HOL/IMPP/Hoare.thy	Sun Nov 28 15:20:51 2010 +0100
     4.3 @@ -367,7 +367,7 @@
     4.4  apply  (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *})
     4.5  apply  (subgoal_tac "G = mgt_call ` U")
     4.6  prefer 2
     4.7 -apply   (simp add: card_seteq finite_imageI)
     4.8 +apply   (simp add: card_seteq)
     4.9  apply  simp
    4.10  apply  (erule prems(3-)) (*MGF_lemma1*)
    4.11  apply (rule ballI)

     5.1 --- a/src/HOL/Library/Infinite_Set.thy	Sat Nov 27 17:44:36 2010 -0800
     5.2 +++ b/src/HOL/Library/Infinite_Set.thy	Sun Nov 28 15:20:51 2010 +0100
     5.3 @@ -339,7 +339,7 @@
     5.4    shows "\<exists>y \<in> f`A. infinite (f -` {y})"
     5.5  proof (rule ccontr)
     5.6    assume "\<not> ?thesis"
     5.7 -  with img have "finite (UN y:f`A. f -` {y})" by (blast intro: finite_UN_I)
     5.8 +  with img have "finite (UN y:f`A. f -` {y})" by blast
     5.9    moreover have "A \<subseteq> (UN y:f`A. f -` {y})" by auto
    5.10    moreover note dom
    5.11    ultimately show False by (simp add: infinite_super)

     6.1 --- a/src/HOL/List.thy	Sat Nov 27 17:44:36 2010 -0800
     6.2 +++ b/src/HOL/List.thy	Sun Nov 28 15:20:51 2010 +0100
     6.3 @@ -3625,7 +3625,7 @@
     6.4    have "?S (Suc n) = (\<Union>x\<in>A. (\<lambda>xs. x#xs) ` ?S n)"
     6.5      by (auto simp:length_Suc_conv)
     6.6    then show ?case using `finite A`
     6.7 -    by (auto intro: finite_imageI Suc) (* FIXME metis? *)
     6.8 +    by (auto intro: Suc) (* FIXME metis? *)
     6.9  qed
    6.10  
    6.11  lemma finite_lists_length_le:

     7.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sat Nov 27 17:44:36 2010 -0800
     7.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Nov 28 15:20:51 2010 +0100
     7.3 @@ -1300,7 +1300,7 @@
     7.4    shows "finite {abs((x::'a::abs ^'n)$i) |i. i\<in> (UNIV :: 'n set)}"
     7.5    and "{abs(x$i) |i. i\<in> (UNIV :: 'n::finite set)} \<noteq> {}"
     7.6    unfolding  infnorm_set_image_cart
     7.7 -  by (auto intro: finite_imageI)
     7.8 +  by auto
     7.9  
    7.10  lemma component_le_infnorm_cart:
    7.11    shows "\<bar>x$i\<bar> \<le> infnorm (x::real^'n)"

     8.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sat Nov 27 17:44:36 2010 -0800
     8.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Nov 28 15:20:51 2010 +0100
     8.3 @@ -2929,7 +2929,7 @@
     8.4        using sf B(3)
     8.5        unfolding span_linear_image[OF lf] surj_def subset_eq image_iff
     8.6        apply blast
     8.7 -      using fB apply (blast intro: finite_imageI)
     8.8 +      using fB apply blast
     8.9        unfolding d[symmetric]
    8.10        apply (rule card_image_le)
    8.11        apply (rule fB)
    8.12 @@ -3035,7 +3035,7 @@
    8.13    shows "finite {abs((x::'a::euclidean_space)$$i) |i. i<DIM('a)}"
    8.14    and "{abs(x$$i) |i. i<DIM('a::euclidean_space)} \<noteq> {}"
    8.15    unfolding infnorm_set_image
    8.16 -  by (auto intro: finite_imageI)
    8.17 +  by auto
    8.18  
    8.19  lemma infnorm_pos_le: "0 \<le> infnorm (x::'a::euclidean_space)"
    8.20    unfolding infnorm_def

     9.1 --- a/src/HOL/Old_Number_Theory/Euler.thy	Sat Nov 27 17:44:36 2010 -0800
     9.2 +++ b/src/HOL/Old_Number_Theory/Euler.thy	Sun Nov 28 15:20:51 2010 +0100
     9.3 @@ -94,7 +94,7 @@
     9.4  subsection {* Properties of SetS *}
     9.5  
     9.6  lemma SetS_finite: "2 < p ==> finite (SetS a p)"
     9.7 -  by (auto simp add: SetS_def SRStar_finite [of p] finite_imageI)
     9.8 +  by (auto simp add: SetS_def SRStar_finite [of p])
     9.9  
    9.10  lemma SetS_elems_finite: "\<forall>X \<in> SetS a p. finite X"
    9.11    by (auto simp add: SetS_def MultInvPair_def)

    10.1 --- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Sat Nov 27 17:44:36 2010 -0800
    10.2 +++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Sun Nov 28 15:20:51 2010 +0100
    10.3 @@ -257,8 +257,7 @@
    10.4    apply (subst setprod_insert)
    10.5      apply (rule_tac [2] Bnor_prod_power_aux)
    10.6       apply (unfold inj_on_def)
    10.7 -     apply (simp_all add: zmult_ac Bnor_fin finite_imageI
    10.8 -       Bnor_mem_zle_swap)
    10.9 +     apply (simp_all add: zmult_ac Bnor_fin Bnor_mem_zle_swap)
   10.10    done
   10.11  
   10.12  

    11.1 --- a/src/HOL/Old_Number_Theory/Finite2.thy	Sat Nov 27 17:44:36 2010 -0800
    11.2 +++ b/src/HOL/Old_Number_Theory/Finite2.thy	Sun Nov 28 15:20:51 2010 +0100
    11.3 @@ -55,7 +55,7 @@
    11.4  subsection {* Cardinality of explicit finite sets *}
    11.5  
    11.6  lemma finite_surjI: "[| B \<subseteq> f ` A; finite A |] ==> finite B"
    11.7 -  by (simp add: finite_subset finite_imageI)
    11.8 +by (simp add: finite_subset)
    11.9  
   11.10  lemma bdd_nat_set_l_finite: "finite {y::nat . y < x}"
   11.11    by (rule bounded_nat_set_is_finite) blast

    12.1 --- a/src/HOL/Old_Number_Theory/Gauss.thy	Sat Nov 27 17:44:36 2010 -0800
    12.2 +++ b/src/HOL/Old_Number_Theory/Gauss.thy	Sun Nov 28 15:20:51 2010 +0100
    12.3 @@ -73,22 +73,22 @@
    12.4    done
    12.5  
    12.6  lemma finite_B: "finite (B)"
    12.7 -  by (auto simp add: B_def finite_A finite_imageI)
    12.8 +by (auto simp add: B_def finite_A)
    12.9  
   12.10  lemma finite_C: "finite (C)"
   12.11 -  by (auto simp add: C_def finite_B finite_imageI)
   12.12 +by (auto simp add: C_def finite_B)
   12.13  
   12.14  lemma finite_D: "finite (D)"
   12.15 -  by (auto simp add: D_def finite_Int finite_C)
   12.16 +by (auto simp add: D_def finite_Int finite_C)
   12.17  
   12.18  lemma finite_E: "finite (E)"
   12.19 -  by (auto simp add: E_def finite_Int finite_C)
   12.20 +by (auto simp add: E_def finite_Int finite_C)
   12.21  
   12.22  lemma finite_F: "finite (F)"
   12.23 -  by (auto simp add: F_def finite_E finite_imageI)
   12.24 +by (auto simp add: F_def finite_E)
   12.25  
   12.26  lemma C_eq: "C = D \<union> E"
   12.27 -  by (auto simp add: C_def D_def E_def)
   12.28 +by (auto simp add: C_def D_def E_def)
   12.29  
   12.30  lemma A_card_eq: "card A = nat ((p - 1) div 2)"
   12.31    apply (auto simp add: A_def)

    13.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Sat Nov 27 17:44:36 2010 -0800
    13.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Sun Nov 28 15:20:51 2010 +0100
    13.3 @@ -511,7 +511,7 @@
    13.4        (\<lambda>(x,y). f -` {x} \<inter> g -` {y} \<inter> space M) ` (f`space M \<times> g`space M)"
    13.5        by auto
    13.6      hence "finite (?p ` (A \<inter> space M))"
    13.7 -      by (rule finite_subset) (auto intro: finite_SigmaI finite_imageI) }
    13.8 +      by (rule finite_subset) auto }
    13.9    note this[intro, simp]
   13.10  
   13.11    { fix x assume "x \<in> space M"

    14.1 --- a/src/HOL/ex/While_Combinator_Example.thy	Sat Nov 27 17:44:36 2010 -0800
    14.2 +++ b/src/HOL/ex/While_Combinator_Example.thy	Sun Nov 28 15:20:51 2010 +0100
    14.3 @@ -28,7 +28,7 @@
    14.4   apply (fastsimp intro!: lfp_lowerbound)
    14.5   apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset])
    14.6  apply (clarsimp simp add: finite_psubset_def order_less_le)
    14.7 -apply (blast intro!: finite_Diff dest: monoD)
    14.8 +apply (blast dest: monoD)
    14.9  done
   14.10  
   14.11