src/HOL/Library/Ramsey.thy

 theory Ramsey
   imports Infinite_Set FuncSet
 begin
 
 subsection \<open>Preliminary definitions\<close>
+
+abbreviation strict_sorted :: "'a::linorder list \<Rightarrow> bool" where
+  "strict_sorted \<equiv> sorted_wrt (<)" 
 
 subsubsection \<open>The $n$-element subsets of a set $A$\<close>
 
 definition nsets :: "['a set, nat] \<Rightarrow> 'a set set" ("([_]\<^bsup>_\<^esup>)" [0,999] 999)
   where "nsets A n \<equiv> {N. N \<subseteq> A \<and> finite N \<and> card N = n}"

     with ij have k: "k = transition_idx s T {?i, ?j}" by (simp add: allk)
     from s_in_T [OF ij] obtain k' where "(s ?j, s ?i) \<in> T k'" "k'<n" by blast
     then show "(s ?j, s ?i) \<in> T k" by (simp add: k transition_idx_in ij)
   qed
   then have "\<not> wf (T k)"
-    by (meson wf_iff_no_infinite_down_chain)
+    unfolding wf_iff_no_infinite_down_chain by iprover
   with wfT \<open>k < n\<close> show False by blast
 qed
 
 end