cleaned up mess
authorhaftmann
Thu Dec 04 16:51:54 2014 +0100 (2014-12-04)
changeset 590949ced35b4a2a9
parent 59093 2b106e58a177
child 59095 3100a7b1c092
cleaned up mess
src/HOL/Hilbert_Choice.thy
src/HOL/Word/Word.thy
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Fri Dec 05 13:39:59 2014 +0100
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu Dec 04 16:51:54 2014 +0100
     1.3 @@ -809,7 +809,6 @@
     1.4    thus ?thesis using bij_betw_id[of A] by auto
     1.5  next
     1.6    assume Case2: "a \<in> A"
     1.7 -find_theorems "\<not> finite _"
     1.8    have "\<not> finite (A - {a})" using INF by auto
     1.9    with infinite_iff_countable_subset[of "A - {a}"] obtain f::"nat \<Rightarrow> 'a"
    1.10    where 1: "inj f" and 2: "f ` UNIV \<le> A - {a}" by blast
     2.1 --- a/src/HOL/Word/Word.thy	Fri Dec 05 13:39:59 2014 +0100
     2.2 +++ b/src/HOL/Word/Word.thy	Thu Dec 04 16:51:54 2014 +0100
     2.3 @@ -63,7 +63,6 @@
     2.4    fix x :: "'a word"
     2.5    assume "\<And>x. PROP P (word_of_int x)"
     2.6    then have "PROP P (word_of_int (uint x))" .
     2.7 -  find_theorems word_of_int uint
     2.8    then show "PROP P x" by (simp add: word_of_int_uint)
     2.9  qed
    2.10