--- a/src/HOL/Infinite_Set.thy Mon Jun 12 22:14:38 2006 +0200
+++ b/src/HOL/Infinite_Set.thy Tue Jun 13 15:07:47 2006 +0200
@@ -11,7 +11,9 @@
subsection "Infinite Sets"
-text {* Some elementary facts about infinite sets, by Stefan Merz. *}
+text {* Some elementary facts about infinite sets, mostly by Stefan Merz.
+Beware! Because "infinite" merely abbreviates a negation, these lemmas may
+not work well with "blast". *}
abbreviation
infinite :: "'a set \<Rightarrow> bool"
@@ -22,9 +24,8 @@
from an infinite set, the result is still infinite.
*}
-lemma infinite_nonempty:
- "\<not> (infinite {})"
- by simp
+lemma infinite_imp_nonempty: "infinite S ==> S \<noteq> {}"
+ by auto
lemma infinite_remove:
"infinite S \<Longrightarrow> infinite (S - {a})"
--- a/src/HOL/Nominal/Nominal.thy Mon Jun 12 22:14:38 2006 +0200
+++ b/src/HOL/Nominal/Nominal.thy Tue Jun 13 15:07:47 2006 +0200
@@ -698,7 +698,7 @@
proof (rule_tac ccontr, drule_tac notnotD)
assume "UNIV-{a} = ({}::'x set)"
with inf2 have "infinite ({}::'x set)" by simp
- then show "False" by (auto intro: infinite_nonempty)
+ then show "False" by auto
qed
hence "\<exists>(b::'x). b\<in>(UNIV-{a})" by blast
then obtain b::"'x" where mem2: "b\<in>(UNIV-{a})" by blast