--- a/src/HOL/Library/Ramsey.thy Mon Nov 25 10:20:25 2013 +0100
+++ b/src/HOL/Library/Ramsey.thy Mon Nov 25 12:27:03 2013 +0100
@@ -247,7 +247,7 @@
then obtain s' and n'
where s': "s' = ?gt n'"
and infeqs': "infinite {n. ?gt n = s'}"
- by (rule inf_img_fin_domE) (auto simp add: vimage_def intro: nat_infinite)
+ by (rule inf_img_fin_domE) (auto simp add: vimage_def intro: infinite_UNIV_nat)
with pg [of n'] have less': "s'<s" by (cases "g n'") auto
have inj_gy: "inj ?gy"
proof (rule linorder_injI)
@@ -410,7 +410,7 @@
have
"\<exists>K k. K \<subseteq> UNIV & infinite K & k < n &
(\<forall>i\<in>K. \<forall>j\<in>K. i\<noteq>j --> transition_idx s T {i,j} = k)"
- by (rule Ramsey2) (auto intro: trless nat_infinite)
+ by (rule Ramsey2) (auto intro: trless infinite_UNIV_nat)
then obtain K and k
where infK: "infinite K" and less: "k < n" and
allk: "\<forall>i\<in>K. \<forall>j\<in>K. i\<noteq>j --> transition_idx s T {i,j} = k"