--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy Thu Sep 17 13:55:21 2020 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy Thu Sep 17 14:27:56 2020 +0200
@@ -422,7 +422,7 @@
lemma field_poly_irreducible_imp_prime:
"prime_elem p" if "irreducible p" for p :: "'a :: field poly"
using that by (fact field_poly.irreducible_imp_prime_elem)
-find_theorems name:prod_mset_prime_factorization
+
lemma field_poly_prod_mset_prime_factorization:
"prod_mset (field_poly.prime_factorization p) = smult (inverse (lead_coeff p)) p"
if "p \<noteq> 0" for p :: "'a :: field poly"
--- a/src/HOL/Real_Asymp/Multiseries_Expansion.thy Thu Sep 17 13:55:21 2020 +0200
+++ b/src/HOL/Real_Asymp/Multiseries_Expansion.thy Thu Sep 17 14:27:56 2020 +0200
@@ -5147,7 +5147,6 @@
lemma filterlim_of_int_at_bot:
"filterlim f F at_bot \<Longrightarrow> filterlim (\<lambda>x. f (of_int x :: real)) F at_bot"
by (erule filterlim_compose[OF _ filterlim_real_of_int_at_bot])
-find_theorems of_int at_bot
lemma asymp_equiv_real_int_transfer_at_top:
"f \<sim>[at_top] g \<Longrightarrow> (\<lambda>x. f (of_int x :: real)) \<sim>[at_top] (\<lambda>x. g (of_int x))"
--- a/src/HOL/Word/Word.thy Thu Sep 17 13:55:21 2020 +0200
+++ b/src/HOL/Word/Word.thy Thu Sep 17 14:27:56 2020 +0200
@@ -2942,7 +2942,7 @@
by (metis mod_pos_pos_trivial uint_lt2p uint_mult_ge0 uint_word_ariths(3))
lemma uint_sub_lem: "uint x \<ge> uint y \<longleftrightarrow> uint (x - y) = uint x - uint y"
- by (metis (mono_tags, hide_lams) diff_ge_0_iff_ge mod_pos_pos_trivial of_nat_0_le_iff take_bit_eq_mod uint_nat uint_sub_lt2p word_sub_wi word_ubin.eq_norm) find_theorems uint \<open>- _\<close>
+ by (metis (mono_tags, hide_lams) diff_ge_0_iff_ge mod_pos_pos_trivial of_nat_0_le_iff take_bit_eq_mod uint_nat uint_sub_lt2p word_sub_wi word_ubin.eq_norm)
lemma uint_add_le: "uint (x + y) \<le> uint x + uint y"
unfolding uint_word_ariths by (simp add: zmod_le_nonneg_dividend)