--- a/src/HOL/Library/Infinite_Set.thy Tue Feb 10 16:09:30 2015 +0000
+++ b/src/HOL/Library/Infinite_Set.thy Tue Feb 10 17:37:06 2015 +0000
@@ -238,7 +238,7 @@
from inf have "infinite {x. P x}" unfolding Inf_many_def .
moreover from q have "{x. P x} \<subseteq> {x. Q x}" by auto
ultimately show ?thesis
- by (simp add: Inf_many_def infinite_super)
+ using Inf_many_def infinite_super by blast
qed
lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x"
--- a/src/HOL/Library/Nat_Bijection.thy Tue Feb 10 16:09:30 2015 +0000
+++ b/src/HOL/Library/Nat_Bijection.thy Tue Feb 10 17:37:06 2015 +0000
@@ -293,6 +293,9 @@
lemma set_encode_empty [simp]: "set_encode {} = 0"
by (simp add: set_encode_def)
+lemma set_encode_inf: "~ finite A \<Longrightarrow> set_encode A = 0"
+ by (simp add: set_encode_def)
+
lemma set_encode_insert [simp]:
"\<lbrakk>finite A; n \<notin> A\<rbrakk> \<Longrightarrow> set_encode (insert n A) = 2^n + set_encode A"
by (simp add: set_encode_def)
--- a/src/HOL/Set.thy Tue Feb 10 16:09:30 2015 +0000
+++ b/src/HOL/Set.thy Tue Feb 10 17:37:06 2015 +0000
@@ -1058,7 +1058,7 @@
"{u. \<exists>x. u = f x} = range f"
by auto
-lemma range_composition:
+lemma range_composition:
"range (\<lambda>x. f (g x)) = f ` range g"
by auto
@@ -1244,7 +1244,7 @@
lemma Collect_conj_eq: "{x. P x & Q x} = {x. P x} \<inter> {x. Q x}"
by blast
-lemma Collect_mono_iff [simp]: "Collect P \<subseteq> Collect Q \<longleftrightarrow> (\<forall>x. P x \<longrightarrow> Q x)"
+lemma Collect_mono_iff: "Collect P \<subseteq> Collect Q \<longleftrightarrow> (\<forall>x. P x \<longrightarrow> Q x)"
by blast
@@ -1809,7 +1809,7 @@
by blast
lemma image_subset_iff_subset_vimage: "f ` A \<subseteq> B \<longleftrightarrow> A \<subseteq> f -` B"
- by blast
+ by blast
lemma vimage_const [simp]: "((\<lambda>x. c) -` A) = (if c \<in> A then UNIV else {})"
by auto