# HG changeset patch
# User paulson
# Date 1150204067 -7200
# Node ID eba1b9e7c45852558117fa8787dcafe8864a40d3
# Parent  e93ffc043dfde398c4d6c3779fab049ac0a3cb9d
removal of the obsolete "infinite_nonempty"

diff -r e93ffc043dfd -r eba1b9e7c458 src/HOL/Infinite_Set.thy
--- 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})"
diff -r e93ffc043dfd -r eba1b9e7c458 src/HOL/Nominal/Nominal.thy
--- 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