--- a/src/HOL/Algebra/Divisibility.thy Wed May 11 10:42:24 2022 +0200
+++ b/src/HOL/Algebra/Divisibility.thy Tue May 17 14:10:14 2022 +0100
@@ -2600,7 +2600,7 @@
next
case (Cons x as)
then have "x \<in> carrier G" "set as \<subseteq> carrier G" and "a divides x \<otimes> foldr (\<otimes>) as \<one>"
- by (auto simp: )
+ by auto
with carr aprime have "a divides x \<or> a divides foldr (\<otimes>) as \<one>"
by (intro prime_divides) simp+
then show ?case
--- a/src/HOL/Analysis/Abstract_Topology.thy Wed May 11 10:42:24 2022 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy Tue May 17 14:10:14 2022 +0100
@@ -3924,7 +3924,7 @@
using \<open>(x, y) \<in> E1 \<times> E2\<close> \<open>x \<in> S\<close> \<open>y \<in> T\<close> by auto
show "(E1 \<inter> S) \<times> (E2 \<inter> T) \<subseteq> U"
using \<open>E1 \<times> E2 \<subseteq> E\<close> \<open>U = _\<close>
- by (auto simp: )
+ by auto
qed
qed
--- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy Wed May 11 10:42:24 2022 +0200
+++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy Tue May 17 14:10:14 2022 +0100
@@ -122,7 +122,7 @@
by (simp add: vimage_Compl diff_eq Int_commute[of "-A"])
also have "{g a..g b} - A = {g a..g b} - A \<inter> {g a..g b}" by blast
also have "emeasure lborel ... = g b - g a - emeasure lborel (A \<inter> {g a..g b})"
- using \<open>A \<in> sets borel\<close> by (subst emeasure_Diff) (auto simp: )
+ using \<open>A \<in> sets borel\<close> by (subst emeasure_Diff) auto
also have "emeasure lborel (A \<inter> {g a..g b}) =
\<integral>\<^sup>+x. indicator A x * indicator {g a..g b} x \<partial>lborel"
using \<open>A \<in> sets borel\<close>
--- a/src/HOL/Analysis/Linear_Algebra.thy Wed May 11 10:42:24 2022 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy Tue May 17 14:10:14 2022 +0100
@@ -1167,7 +1167,7 @@
next
assume ?rhs
then obtain u v where *: "\<And>x. x \<in> S \<Longrightarrow> \<exists>c. x = u + c *\<^sub>R v"
- by (auto simp: )
+ by auto
have "\<exists>c. x - y = c *\<^sub>R v" if "x \<in> S" "y \<in> S" for x y
by (metis *[OF \<open>x \<in> S\<close>] *[OF \<open>y \<in> S\<close>] scaleR_left.diff add_diff_cancel_left)
then show ?lhs
--- a/src/HOL/Analysis/Lipschitz.thy Wed May 11 10:42:24 2022 +0200
+++ b/src/HOL/Analysis/Lipschitz.thy Tue May 17 14:10:14 2022 +0100
@@ -623,7 +623,7 @@
by (simp add: dist_commute)
subgoal
using \<open>0 < u\<close> \<open>b \<in> X\<close>
- by (simp add: )
+ by simp
done
also have "(L + 1) * dist y b \<le> e / 2"
using le1 \<open>0 \<le> L\<close> by simp
--- a/src/HOL/Analysis/T1_Spaces.thy Wed May 11 10:42:24 2022 +0200
+++ b/src/HOL/Analysis/T1_Spaces.thy Tue May 17 14:10:14 2022 +0100
@@ -289,7 +289,7 @@
by metis
with \<open>a \<notin> T\<close> compactin_subset_topspace [OF T]
have Topen: "\<forall>W \<in> U ` T. openin X W" and Tsub: "T \<subseteq> \<Union> (U ` T)"
- by (auto simp: )
+ by auto
then obtain \<F> where \<F>: "finite \<F>" "\<F> \<subseteq> U ` T" and "T \<subseteq> \<Union>\<F>"
using T unfolding compactin_def by meson
then obtain F where F: "finite F" "F \<subseteq> T" "\<F> = U ` F" and SUF: "T \<subseteq> \<Union>(U ` F)" and "a \<notin> F"
--- a/src/HOL/Complex_Analysis/Winding_Numbers.thy Wed May 11 10:42:24 2022 +0200
+++ b/src/HOL/Complex_Analysis/Winding_Numbers.thy Tue May 17 14:10:14 2022 +0100
@@ -1316,7 +1316,7 @@
also have "... < e"
using \<open>e>0\<close> by (auto simp: norm_mult intro: le_less_trans [OF norm_triangle_ineq4])
finally have "z \<in> ball 0 e"
- using \<open>e>0\<close> by (simp add: )
+ using \<open>e>0\<close> by simp
then have "Im z * Re b \<le> Im b * Re z"
using e by blast
then have b: "0 < Re b" "0 < Im b" and disj: "e * Re b < - (Im b * e) \<or> e * Re b = - (Im b * e)"
--- a/src/HOL/Computational_Algebra/Nth_Powers.thy Wed May 11 10:42:24 2022 +0200
+++ b/src/HOL/Computational_Algebra/Nth_Powers.thy Tue May 17 14:10:14 2022 +0100
@@ -279,7 +279,7 @@
lemma nth_root_nat_naive_code [code]:
"nth_root_nat m n = (if m = 0 \<or> n = 0 then 0 else if m = 1 \<or> n = 1 then n else
nth_root_nat_aux m 1 1 n)"
- using nth_root_nat_aux_correct[of 1 m n] by (auto simp: )
+ using nth_root_nat_aux_correct[of 1 m n] by auto
lemma nth_root_nat_nth_power [simp]: "k > 0 \<Longrightarrow> nth_root_nat k (n ^ k) = n"
--- a/src/HOL/Decision_Procs/Approximation_Bounds.thy Wed May 11 10:42:24 2022 +0200
+++ b/src/HOL/Decision_Procs/Approximation_Bounds.thy Tue May 17 14:10:14 2022 +0100
@@ -333,7 +333,7 @@
"x * y \<in>\<^sub>r mult_float_interval prec A B"
if "x \<in>\<^sub>i real_interval A" "y \<in>\<^sub>i real_interval B"
using mult_float_interval[of A B] that
- by (auto simp: )
+ by auto
lemma mult_float_interval_mono':
"set_of (mult_float_interval prec A B) \<subseteq> set_of (mult_float_interval prec X Y)"
--- a/src/HOL/Library/Interval.thy Wed May 11 10:42:24 2022 +0200
+++ b/src/HOL/Library/Interval.thy Tue May 17 14:10:14 2022 +0100
@@ -751,8 +751,8 @@
and upper_split_interval2: "upper (snd (split_interval X m)) = max (upper X) m"
subgoal by transfer auto
subgoal by transfer (auto simp: min.commute)
- subgoal by transfer (auto simp: )
- subgoal by transfer (auto simp: )
+ subgoal by transfer auto
+ subgoal by transfer auto
done
lemma split_intervalD: "split_interval X x = (A, B) \<Longrightarrow> set_of X \<subseteq> set_of A \<union> set_of B"
--- a/src/HOL/Library/Log_Nat.thy Wed May 11 10:42:24 2022 +0200
+++ b/src/HOL/Library/Log_Nat.thy Tue May 17 14:10:14 2022 +0100
@@ -183,7 +183,7 @@
proof -
have "0 \<le> log (real b) (real x)"
using \<open>b > 1\<close> \<open>0 < x\<close>
- by (auto simp: )
+ by auto
then have "?l \<le> b powr log (real b) (real x)"
using \<open>b > 1\<close>
by (auto simp flip: powr_realpow intro!: powr_mono of_nat_floor)
--- a/src/HOL/Library/Poly_Mapping.thy Wed May 11 10:42:24 2022 +0200
+++ b/src/HOL/Library/Poly_Mapping.thy Tue May 17 14:10:14 2022 +0100
@@ -1688,7 +1688,7 @@
lemma keys_cmul_iff [iff]: "i \<in> Poly_Mapping.keys (frag_cmul c x) \<longleftrightarrow> i \<in> Poly_Mapping.keys x \<and> c \<noteq> 0"
- apply (auto simp: )
+ apply auto
apply (meson subsetD keys_cmul)
by (metis in_keys_iff lookup_frag_cmul mult_eq_0_iff)
--- a/src/HOL/Probability/Distributions.thy Wed May 11 10:42:24 2022 +0200
+++ b/src/HOL/Probability/Distributions.thy Tue May 17 14:10:14 2022 +0100
@@ -1332,7 +1332,7 @@
shows "expectation X = 0"
using integral_std_normal_moment_odd[of 0]
distributed_integral[OF D, of "\<lambda>x. x", symmetric]
- by (auto simp: )
+ by auto
lemma (in prob_space) normal_distributed_expectation:
assumes \<sigma>[arith]: "0 < \<sigma>"
--- a/src/HOL/Probability/Product_PMF.thy Wed May 11 10:42:24 2022 +0200
+++ b/src/HOL/Probability/Product_PMF.thy Tue May 17 14:10:14 2022 +0100
@@ -354,7 +354,7 @@
Pi_pmf A dflt' (\<lambda>x. g x \<bind> (\<lambda>x. return_pmf (f x)))"
using assms by (simp add: map_pmf_def Pi_pmf_bind)
also have "\<dots> = Pi_pmf A dflt g \<bind> (\<lambda>h. return_pmf (\<lambda>x. if x \<in> A then f (h x) else dflt'))"
- by (subst Pi_pmf_bind[where d' = dflt]) (auto simp: )
+ by (subst Pi_pmf_bind[where d' = dflt]) auto
also have "\<dots> = map_pmf (\<lambda>h. f \<circ> h) (Pi_pmf A dflt g)"
unfolding map_pmf_def using set_Pi_pmf_subset'[of A dflt g]
by (intro bind_pmf_cong refl arg_cong[of _ _ return_pmf])
--- a/src/HOL/Probability/Stream_Space.thy Wed May 11 10:42:24 2022 +0200
+++ b/src/HOL/Probability/Stream_Space.thy Tue May 17 14:10:14 2022 +0100
@@ -493,7 +493,7 @@
proof (safe intro!: sets_Sup_in_sets del: subsetI equalityI)
fix i :: nat
show "space (?V i) = space ?R"
- using scylinder_streams by (subst space_measure_of) (auto simp: )
+ using scylinder_streams by (subst space_measure_of) auto
{ fix A assume "A \<in> G"
then have "scylinder (space S) (replicate i (space S) @ [A]) = (\<lambda>s. s !! i) -` A \<inter> streams (space S)"
by (induction i) (auto simp add: streams_shd streams_stl cong: conj_cong)
--- a/src/HOL/Quotient.thy Wed May 11 10:42:24 2022 +0200
+++ b/src/HOL/Quotient.thy Tue May 17 14:10:14 2022 +0100
@@ -576,7 +576,7 @@
using r Quotient3_refl1 R1 rep_abs_rsp by fastforce
moreover have "R2' (Rep1 (Abs1 r)) (Rep1 (Abs1 s))"
using that
- apply (simp add: )
+ apply simp
apply (metis (full_types) Rep1 Abs1 Quotient3_rel R2 Quotient3_refl1 [OF R1] Quotient3_refl2 [OF R1] Quotient3_rel_abs [OF R1])
done
moreover have "R1 (Rep1 (Abs1 s)) s"
--- a/src/HOL/Rings.thy Wed May 11 10:42:24 2022 +0200
+++ b/src/HOL/Rings.thy Tue May 17 14:10:14 2022 +0100
@@ -2408,7 +2408,7 @@
proof (rule ccontr, simp add: not_less)
assume "b \<le> a"
with that show False
- by (simp add: )
+ by simp
qed
qed
--- a/src/HOL/Set_Interval.thy Wed May 11 10:42:24 2022 +0200
+++ b/src/HOL/Set_Interval.thy Tue May 17 14:10:14 2022 +0100
@@ -465,7 +465,7 @@
apply (auto simp:subset_eq Ball_def not_le)
apply(frule_tac x=a in spec)
apply(erule_tac x=d in allE)
- apply (auto simp: )
+ apply auto
done
lemma atLeastLessThan_inj: