--- a/src/HOL/Algebra/Cycles.thy Tue Jun 16 08:41:39 2020 +0000
+++ b/src/HOL/Algebra/Cycles.thy Tue Jun 16 08:41:39 2020 +0000
@@ -160,7 +160,7 @@
using aui_lemma[OF assms] by simp
next
case 2 thus ?thesis
- using aui_lemma[OF assms(2,1)] assms(3) by (simp add: ac_simps(8))
+ using aui_lemma[OF assms(2,1)] assms(3) by (simp add: ac_simps)
next
case 3 thus ?thesis
by (simp add: id_outside_supp)
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Tue Jun 16 08:41:39 2020 +0000
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Tue Jun 16 08:41:39 2020 +0000
@@ -2015,8 +2015,8 @@
"min (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) = (if 0 < m i then m i * (a \<bullet> i) else m i * (b \<bullet> i))"
"max (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) = (if 0 < m i then m i * (b \<bullet> i) else m i * (a \<bullet> i))"
using a_le_b by (auto simp: min_def max_def mult_le_cancel_left)
- with False show ?thesis using a_le_b
- unfolding * by (auto simp: le_divide_eq divide_le_eq ac_simps)
+ with False show ?thesis using a_le_b *
+ by (simp add: le_divide_eq divide_le_eq) (simp add: ac_simps)
qed
qed
qed simp
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue Jun 16 08:41:39 2020 +0000
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue Jun 16 08:41:39 2020 +0000
@@ -2545,8 +2545,7 @@
lemma comm_monoid_set_F_and: "comm_monoid_set.F (\<and>) True f s \<longleftrightarrow> (finite s \<longrightarrow> (\<forall>x\<in>s. f x))"
proof -
- interpret bool: comm_monoid_set "(\<and>)" True
- proof qed auto
+ interpret bool: comm_monoid_set \<open>(\<and>)\<close> True ..
show ?thesis
by (induction s rule: infinite_finite_induct) auto
qed
--- a/src/HOL/Lattices.thy Tue Jun 16 08:41:39 2020 +0000
+++ b/src/HOL/Lattices.thy Tue Jun 16 08:41:39 2020 +0000
@@ -145,16 +145,16 @@
end
-text \<open>Passive interpretations for boolean operators\<close>
+text \<open>Interpretations for boolean operators\<close>
-lemma semilattice_neutr_and:
- "semilattice_neutr HOL.conj True"
+interpretation conj: semilattice_neutr \<open>(\<and>)\<close> True
by standard auto
-lemma semilattice_neutr_or:
- "semilattice_neutr HOL.disj False"
+interpretation disj: semilattice_neutr \<open>(\<or>)\<close> False
by standard auto
+declare conj_assoc [ac_simps del] disj_assoc [ac_simps del] \<comment> \<open>already simp by default\<close>
+
subsection \<open>Syntactic infimum and supremum operations\<close>
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Tue Jun 16 08:41:39 2020 +0000
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Tue Jun 16 08:41:39 2020 +0000
@@ -353,7 +353,7 @@
using J by (intro emeasure_PiM_emb) (simp_all add: finite_vimageI inj_on_def)
also have "\<dots> = (\<Prod>j\<in>J - (J \<inter> {..<i}). emeasure M (E j))"
by (rule prod.reindex_cong [of "\<lambda>x. x - i"])
- (auto simp: image_iff Bex_def not_less nat_eq_diff_eq ac_simps cong: conj_cong intro!: inj_onI)
+ (auto simp: image_iff ac_simps nat_eq_diff_eq cong: conj_cong intro!: inj_onI)
also have "emeasure S ?E = (\<Prod>j\<in>J \<inter> {..<i}. emeasure M (E j))"
using J by (intro emeasure_PiM_emb) simp_all
also have "(\<Prod>j\<in>J \<inter> {..<i}. emeasure M (E j)) * (\<Prod>j\<in>J - (J \<inter> {..<i}). emeasure M (E j)) = (\<Prod>j\<in>J. emeasure M (E j))"
@@ -384,7 +384,7 @@
using J by (intro emeasure_PiM_emb) (simp_all add: finite_vimageI)
also have "\<dots> = (\<Prod>j\<in>J - {0}. emeasure M (E j))"
by (rule prod.reindex_cong [of "\<lambda>x. x - 1"])
- (auto simp: image_iff Bex_def not_less nat_eq_diff_eq ac_simps cong: conj_cong intro!: inj_onI)
+ (auto simp: image_iff nat_eq_diff_eq ac_simps cong: conj_cong intro!: inj_onI)
also have "emeasure M ?E * (\<Prod>j\<in>J - {0}. emeasure M (E j)) = (\<Prod>j\<in>J. emeasure M (E j))"
by (auto simp: M.emeasure_space_1 prod.remove J)
finally show "emeasure ?D ?X = (\<Prod>j\<in>J. emeasure M (E j))" .