src/HOL/Library/Ramsey.thy

 
 subsection {* Disjunctive Well-Foundedness *}
 
 text {*
   An application of Ramsey's theorem to program termination. See
-  \cite{Podelski-Rybalchenko}.
+  @{cite "Podelski-Rybalchenko"}.
 *}
 
 definition disj_wf :: "('a * 'a)set => bool"
   where "disj_wf r = (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r = (\<Union>i<n. T i))"