# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1423589826 0
# Node ID 4af6076523180f76c0d4fec01e906f2ef51b8dda
# Parent  d64d48eb71cc206152b5e970f247a7e28e1491ad
Not a simprule, as it complicates proofs

diff -r d64d48eb71cc -r 4af607652318 src/HOL/Library/Infinite_Set.thy
--- 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"
diff -r d64d48eb71cc -r 4af607652318 src/HOL/Library/Nat_Bijection.thy
--- 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)
diff -r d64d48eb71cc -r 4af607652318 src/HOL/Set.thy
--- 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