# HG changeset patch # User berghofe # Date 1184147565 -7200 # Node ID 2215169c93fa867477e895bd90b5ed7fa64065aa # Parent 8b37b6615c5257739ceff7728b126ee53b745b8c renamed inductive2 to inductive. diff -r 8b37b6615c52 -r 2215169c93fa src/HOL/ex/Primrec.thy --- 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') (\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)"