src/HOL/Library/Ramsey.thy
changeset 22367 6860f09242bf
parent 21634 369e38e35686
child 22665 cf152ff55d16
     1.1 --- a/src/HOL/Library/Ramsey.thy	Tue Feb 27 00:32:52 2007 +0100
     1.2 +++ b/src/HOL/Library/Ramsey.thy	Tue Feb 27 00:33:49 2007 +0100
     1.3 @@ -235,10 +235,9 @@
     1.4  
     1.5  subsection {*Disjunctive Well-Foundedness*}
     1.6  
     1.7 -text{*An application of Ramsey's theorem to program termination. See
     1.8 -
     1.9 -Andreas Podelski and Andrey Rybalchenko, Transition Invariants, 19th Annual
    1.10 -IEEE Symposium on Logic in Computer Science (LICS'04), pages 32--41 (2004).
    1.11 +text {*
    1.12 +  An application of Ramsey's theorem to program termination. See
    1.13 +  \cite{Podelski-Rybalchenko}.
    1.14  *}
    1.15  
    1.16  definition