author | berghofe |
Wed, 11 Jul 2007 11:52:45 +0200 | |
changeset 23776 | 2215169c93fa |
parent 23775 | 8b37b6615c52 |
child 23777 | 60b7800338d5 |
--- a/src/HOL/ex/Primrec.thy Wed Jul 11 11:52:28 2007 +0200 +++ b/src/HOL/ex/Primrec.thy Wed Jul 11 11:52:45 2007 +0200 @@ -66,7 +66,7 @@ | x # l' => nat_rec (f l') (\<lambda>y r. g (r # y # l')) x)" -- {* Note that @{term g} is applied first to @{term "PREC f g y"} and then to @{term y}! *} -inductive2 PRIMREC :: "(nat list => nat) => bool" +inductive PRIMREC :: "(nat list => nat) => bool" where SC: "PRIMREC SC" | CONSTANT: "PRIMREC (CONSTANT k)"