# HG changeset patch
# User haftmann
# Date 1600345676 -7200
# Node ID ff32ddc8165c7d584e5f5cb5a72ba7053813bfb8
# Parent  47253b1a31ed97b8b684731ecea57e691a3a06ed
dropped junk

diff -r 47253b1a31ed -r ff32ddc8165c src/HOL/Computational_Algebra/Polynomial_Factorial.thy
--- 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"
diff -r 47253b1a31ed -r ff32ddc8165c src/HOL/Real_Asymp/Multiseries_Expansion.thy
--- 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))"
diff -r 47253b1a31ed -r ff32ddc8165c src/HOL/Word/Word.thy
--- 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)