# HG changeset patch
# User haftmann
# Date 1417708314 -3600
# Node ID 9ced35b4a2a961dfb3c507274e349c246d04fbe8
# Parent  2b106e58a177bf1377be0b3daf92512714bc7fba
cleaned up mess

diff -r 2b106e58a177 -r 9ced35b4a2a9 src/HOL/Hilbert_Choice.thy
--- 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
diff -r 2b106e58a177 -r 9ced35b4a2a9 src/HOL/Word/Word.thy
--- 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