1.1 --- a/src/HOL/Finite_Set.thy	Tue Mar 13 12:51:52 2012 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Mar 13 13:31:26 2012 +0100
     1.3 @@ -22,7 +22,8 @@
     1.4    assumes "P {}"
     1.5      and insert: "\<And>x F. finite F \<Longrightarrow> x \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert x F)"
     1.6    shows "P F"
     1.7 -using `finite F` proof induct
     1.8 +using `finite F`
     1.9 +proof induct
    1.10    show "P {}" by fact
    1.11    fix x F assume F: "finite F" and P: "P F"
    1.12    show "P (insert x F)"
    1.13 @@ -68,7 +69,8 @@
    1.14  lemma finite_imp_nat_seg_image_inj_on:
    1.15    assumes "finite A" 
    1.16    shows "\<exists>(n::nat) f. A = f ` {i. i < n} \<and> inj_on f {i. i < n}"
    1.17 -using assms proof induct
    1.18 +using assms
    1.19 +proof induct
    1.20    case empty
    1.21    show ?case
    1.22    proof
    1.23 @@ -248,7 +250,8 @@
    1.24  lemma finite_imageD:
    1.25    assumes "finite (f ` A)" and "inj_on f A"
    1.26    shows "finite A"
    1.27 -using assms proof (induct "f ` A" arbitrary: A)
    1.28 +using assms
    1.29 +proof (induct "f ` A" arbitrary: A)
    1.30    case empty then show ?case by simp
    1.31  next
    1.32    case (insert x B)
    1.33 @@ -272,7 +275,8 @@
    1.34  lemma finite_subset_image:
    1.35    assumes "finite B"
    1.36    shows "B \<subseteq> f ` A \<Longrightarrow> \<exists>C\<subseteq>A. finite C \<and> B = f ` C"
    1.37 -using assms proof induct
    1.38 +using assms
    1.39 +proof induct
    1.40    case empty then show ?case by simp
    1.41  next
    1.42    case insert then show ?case
    1.43 @@ -413,7 +417,8 @@
    1.44    assumes "\<And>x. P {x}"
    1.45      and "\<And>x F. finite F \<Longrightarrow> F \<noteq> {} \<Longrightarrow> x \<notin> F \<Longrightarrow> P F  \<Longrightarrow> P (insert x F)"
    1.46    shows "P F"
    1.47 -using assms proof induct
    1.48 +using assms
    1.49 +proof induct
    1.50    case empty then show ?case by simp
    1.51  next
    1.52    case (insert x F) then show ?case by cases auto
    1.53 @@ -424,7 +429,8 @@
    1.54    assumes empty: "P {}"
    1.55      and insert: "\<And>a F. finite F \<Longrightarrow> a \<in> A \<Longrightarrow> a \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert a F)"
    1.56    shows "P F"
    1.57 -using `finite F` `F \<subseteq> A` proof induct
    1.58 +using `finite F` `F \<subseteq> A`
    1.59 +proof induct
    1.60    show "P {}" by fact
    1.61  next
    1.62    fix x F
    1.63 @@ -486,8 +492,8 @@
    1.64  
    1.65  end
    1.66  
    1.67 -instance prod :: (finite, finite) finite proof
    1.68 -qed (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
    1.69 +instance prod :: (finite, finite) finite
    1.70 +  by default (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
    1.71  
    1.72  lemma inj_graph: "inj (%f. {(x, y). y = f x})"
    1.73    by (rule inj_onI, auto simp add: set_eq_iff fun_eq_iff)
    1.74 @@ -506,24 +512,24 @@
    1.75    qed
    1.76  qed
    1.77  
    1.78 -instance bool :: finite proof
    1.79 -qed (simp add: UNIV_bool)
    1.80 +instance bool :: finite
    1.81 +  by default (simp add: UNIV_bool)
    1.82  
    1.83  instance set :: (finite) finite
    1.84    by default (simp only: Pow_UNIV [symmetric] finite_Pow_iff finite)
    1.85  
    1.86 -instance unit :: finite proof
    1.87 -qed (simp add: UNIV_unit)
    1.88 +instance unit :: finite
    1.89 +  by default (simp add: UNIV_unit)
    1.90  
    1.91 -instance sum :: (finite, finite) finite proof
    1.92 -qed (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
    1.93 +instance sum :: (finite, finite) finite
    1.94 +  by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
    1.95  
    1.96  lemma finite_option_UNIV [simp]:
    1.97    "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)"
    1.98    by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some)
    1.99  
   1.100 -instance option :: (finite) finite proof
   1.101 -qed (simp add: UNIV_option_conv)
   1.102 +instance option :: (finite) finite
   1.103 +  by default (simp add: UNIV_option_conv)
   1.104  
   1.105  
   1.106  subsection {* A basic fold functional for finite sets *}
   1.107 @@ -830,9 +836,9 @@
   1.108    assumes "finite A" and "a \<notin> A"
   1.109    shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)"
   1.110  proof -
   1.111 -  interpret comp_fun_commute "%x y. (g x) * y" proof
   1.112 -  qed (simp add: fun_eq_iff mult_ac)
   1.113 -  show ?thesis using assms by (simp add: fold_image_def)
   1.114 +  interpret comp_fun_commute "%x y. (g x) * y"
   1.115 +    by default (simp add: fun_eq_iff mult_ac)
   1.116 +  from assms show ?thesis by (simp add: fold_image_def)
   1.117  qed
   1.118  
   1.119  lemma fold_image_reindex:
   1.120 @@ -1018,8 +1024,8 @@
   1.121  context ab_semigroup_mult
   1.122  begin
   1.123  
   1.124 -lemma comp_fun_commute: "comp_fun_commute (op *)" proof
   1.125 -qed (simp add: fun_eq_iff mult_ac)
   1.126 +lemma comp_fun_commute: "comp_fun_commute (op *)"
   1.127 +  by default (simp add: fun_eq_iff mult_ac)
   1.128  
   1.129  lemma fold_graph_insert_swap:
   1.130  assumes fold: "fold_graph times (b::'a) A y" and "b \<notin> A"
   1.131 @@ -1104,8 +1110,8 @@
   1.132  context ab_semigroup_idem_mult
   1.133  begin
   1.134  
   1.135 -lemma comp_fun_idem: "comp_fun_idem (op *)" proof
   1.136 -qed (simp_all add: fun_eq_iff mult_left_commute)
   1.137 +lemma comp_fun_idem: "comp_fun_idem (op *)"
   1.138 +  by default (simp_all add: fun_eq_iff mult_left_commute)
   1.139  
   1.140  lemma fold1_insert_idem [simp]:
   1.141    assumes nonempty: "A \<noteq> {}" and A: "finite A" 
   1.142 @@ -1137,7 +1143,8 @@
   1.143  lemma hom_fold1_commute:
   1.144  assumes hom: "!!x y. h (x * y) = h x * h y"
   1.145  and N: "finite N" "N \<noteq> {}" shows "h (fold1 times N) = fold1 times (h ` N)"
   1.146 -using N proof (induct rule: finite_ne_induct)
   1.147 +using N
   1.148 +proof (induct rule: finite_ne_induct)
   1.149    case singleton thus ?case by simp
   1.150  next
   1.151    case (insert n N)
   1.152 @@ -1293,8 +1300,8 @@
   1.153    assumes "finite A" and "x \<notin> A"
   1.154    shows "F (insert x A) = F A \<circ> f x"
   1.155  proof -
   1.156 -  interpret comp_fun_commute f proof
   1.157 -  qed (insert comp_fun_commute, simp add: fun_eq_iff)
   1.158 +  interpret comp_fun_commute f
   1.159 +    by default (insert comp_fun_commute, simp add: fun_eq_iff)
   1.160    from fold_insert2 assms
   1.161    have "\<And>s. fold f s (insert x A) = fold f (f x s) A" .
   1.162    with `finite A` show ?thesis by (simp add: eq_fold fun_eq_iff)
   1.163 @@ -1426,9 +1433,9 @@
   1.164    assumes "finite A" and "x \<notin> A"
   1.165    shows "F (insert x A) = g x * F A"
   1.166  proof -
   1.167 -  interpret comp_fun_commute "%x y. (g x) * y" proof
   1.168 -  qed (simp add: ac_simps fun_eq_iff)
   1.169 -  with assms have "fold_image (op *) g 1 (insert x A) = g x * fold_image (op *) g 1 A"
   1.170 +  interpret comp_fun_commute "%x y. (g x) * y"
   1.171 +    by default (simp add: ac_simps fun_eq_iff)
   1.172 +  from assms have "fold_image (op *) g 1 (insert x A) = g x * fold_image (op *) g 1 A"
   1.173      by (simp add: fold_image_def)
   1.174    with `finite A` show ?thesis by (simp add: eq_fold_g)
   1.175  qed
   1.176 @@ -1650,8 +1657,8 @@
   1.177    assumes "finite A" and "x \<notin> A"
   1.178    shows "F (insert x A) = fold (op *) x A"
   1.179  proof -
   1.180 -  interpret ab_semigroup_mult "op *" proof qed (simp_all add: ac_simps)
   1.181 -  with assms show ?thesis by (simp add: eq_fold fold1_eq_fold)
   1.182 +  interpret ab_semigroup_mult "op *" by default (simp_all add: ac_simps)
   1.183 +  from assms show ?thesis by (simp add: eq_fold fold1_eq_fold)
   1.184  qed
   1.185  
   1.186  lemma insert [simp]:
   1.187 @@ -1756,8 +1763,8 @@
   1.188    assumes "finite A"
   1.189    shows "F (insert a A) = fold (op *) a A"
   1.190  proof -
   1.191 -  interpret ab_semigroup_idem_mult "op *" proof qed (simp_all add: ac_simps)
   1.192 -  with assms show ?thesis by (simp add: eq_fold fold1_eq_fold_idem)
   1.193 +  interpret ab_semigroup_idem_mult "op *" by default (simp_all add: ac_simps)
   1.194 +  from assms show ?thesis by (simp add: eq_fold fold1_eq_fold_idem)
   1.195  qed
   1.196  
   1.197  lemma insert_idem [simp]:

     2.1 --- a/src/HOL/List.thy	Tue Mar 13 12:51:52 2012 +0100
     2.2 +++ b/src/HOL/List.thy	Tue Mar 13 13:31:26 2012 +0100
     2.3 @@ -4483,7 +4483,8 @@
     2.4    shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
     2.5  proof -
     2.6    interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
     2.7 -  with assms show ?thesis by (simp add: sorted_list_of_set_def fold_insert_remove)
     2.8 +  from assms show ?thesis
     2.9 +    by (simp add: sorted_list_of_set_def fold_insert_remove)
    2.10  qed
    2.11  
    2.12  lemma sorted_list_of_set [simp]:

     3.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Mar 13 12:51:52 2012 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Mar 13 13:31:26 2012 +0100
     3.3 @@ -1689,7 +1689,7 @@
     3.4  proof
     3.5    assume ?l guess f' using `?l`[unfolded differentiable_def] .. note f' = this
     3.6    then interpret bounded_linear f' by auto
     3.7 -  thus ?r unfolding vector_derivative_def has_vector_derivative_def
     3.8 +  show ?r unfolding vector_derivative_def has_vector_derivative_def
     3.9      apply-apply(rule someI_ex,rule_tac x="f' 1" in exI)
    3.10      using f' unfolding scaleR[THEN sym] by auto
    3.11  next

     4.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Tue Mar 13 12:51:52 2012 +0100
     4.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Tue Mar 13 13:31:26 2012 +0100
     4.3 @@ -197,7 +197,7 @@
     4.4  next
     4.5    fix A assume "A \<in> sets (M2 \<Otimes>\<^isub>M M1)"
     4.6    interpret Q: pair_sigma_algebra M2 M1 by default
     4.7 -  with Q.sets_pair_sigma_algebra_swap[OF `A \<in> sets (M2 \<Otimes>\<^isub>M M1)`]
     4.8 +  from Q.sets_pair_sigma_algebra_swap[OF `A \<in> sets (M2 \<Otimes>\<^isub>M M1)`]
     4.9    show "?f -` A \<inter> space ?P \<in> sets ?P" by simp
    4.10  qed
    4.11  
    4.12 @@ -221,7 +221,7 @@
    4.13    assumes Q: "Q \<in> sets P" shows "(\<lambda>x. (x, y)) -` Q \<in> sets M1" (is "?cut Q \<in> sets M1")
    4.14  proof -
    4.15    interpret Q: pair_sigma_algebra M2 M1 by default
    4.16 -  with Q.measurable_cut_fst[OF sets_pair_sigma_algebra_swap[OF Q], of y]
    4.17 +  from Q.measurable_cut_fst[OF sets_pair_sigma_algebra_swap[OF Q], of y]
    4.18    show ?thesis by (simp add: vimage_compose[symmetric] comp_def)
    4.19  qed
    4.20  

     5.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Tue Mar 13 12:51:52 2012 +0100
     5.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Tue Mar 13 13:31:26 2012 +0100
     5.3 @@ -858,7 +858,7 @@
     5.4  using assms proof induct
     5.5    case empty
     5.6    interpret finite_product_sigma_finite M "{}" by default auto
     5.7 -  then show ?case by simp
     5.8 +  show ?case by simp
     5.9  next
    5.10    case (insert i I)
    5.11    note `finite I`[intro, simp]

     6.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Mar 13 12:51:52 2012 +0100
     6.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Mar 13 13:31:26 2012 +0100
     6.3 @@ -502,7 +502,7 @@
     6.4      fix A assume "A \<in> sets ?G"
     6.5      with generatorE guess J X . note JX = this
     6.6      interpret JK: finite_product_prob_space M J by default fact+
     6.7 -    with JX show "\<mu>G A \<noteq> \<infinity>" by simp
     6.8 +    from JX show "\<mu>G A \<noteq> \<infinity>" by simp
     6.9    next
    6.10      fix A assume A: "range A \<subseteq> sets ?G" "decseq A" "(\<Inter>i. A i) = {}"
    6.11      then have "decseq (\<lambda>i. \<mu>G (A i))"

     7.1 --- a/src/HOL/Probability/Probability_Measure.thy	Tue Mar 13 12:51:52 2012 +0100
     7.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Tue Mar 13 13:31:26 2012 +0100
     7.3 @@ -622,7 +622,7 @@
     7.4    assumes "finite_random_variable M' X" shows "random_variable M' X"
     7.5  proof -
     7.6    interpret M': finite_sigma_algebra M' using assms by simp
     7.7 -  then show "random_variable M' X" using assms by simp default
     7.8 +  show "random_variable M' X" using assms by simp default
     7.9  qed
    7.10  
    7.11  lemma (in prob_space) distribution_finite_prob_space: