--- a/src/HOL/Library/Ramsey.thy Sat Jan 16 17:15:27 2010 +0100
+++ b/src/HOL/Library/Ramsey.thy Sat Jan 16 17:15:28 2010 +0100
@@ -12,13 +12,10 @@
subsubsection {* ``Axiom'' of Dependent Choice *}
-consts choice :: "('a => bool) => ('a * 'a) set => nat => 'a"
+primrec choice :: "('a => bool) => ('a * 'a) set => nat => 'a" where
--{*An integer-indexed chain of choices*}
-primrec
- choice_0: "choice P r 0 = (SOME x. P x)"
-
- choice_Suc: "choice P r (Suc n) = (SOME y. P y & (choice P r n, y) \<in> r)"
-
+ choice_0: "choice P r 0 = (SOME x. P x)"
+ | choice_Suc: "choice P r (Suc n) = (SOME y. P y & (choice P r n, y) \<in> r)"
lemma choice_n:
assumes P0: "P x0"