--- a/src/HOL/Hilbert_Choice.thy Fri Dec 05 13:39:59 2014 +0100
+++ b/src/HOL/Hilbert_Choice.thy Thu Dec 04 16:51:54 2014 +0100
@@ -809,7 +809,6 @@
thus ?thesis using bij_betw_id[of A] by auto
next
assume Case2: "a \<in> A"
-find_theorems "\<not> finite _"
have "\<not> finite (A - {a})" using INF by auto
with infinite_iff_countable_subset[of "A - {a}"] obtain f::"nat \<Rightarrow> 'a"
where 1: "inj f" and 2: "f ` UNIV \<le> A - {a}" by blast
--- a/src/HOL/Word/Word.thy Fri Dec 05 13:39:59 2014 +0100
+++ b/src/HOL/Word/Word.thy Thu Dec 04 16:51:54 2014 +0100
@@ -63,7 +63,6 @@
fix x :: "'a word"
assume "\<And>x. PROP P (word_of_int x)"
then have "PROP P (word_of_int (uint x))" .
- find_theorems word_of_int uint
then show "PROP P x" by (simp add: word_of_int_uint)
qed