| changeset 11696 | 233362cfecc7 |
| parent 11679 | afdbee613f58 |
| child 11726 | 2b2a45abe876 |
--- a/src/FOL/ex/Natural_Numbers.thy Fri Oct 05 21:37:33 2001 +0200 +++ b/src/FOL/ex/Natural_Numbers.thy Fri Oct 05 21:42:10 2001 +0200 @@ -17,7 +17,7 @@ rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a" axioms - induct [induct type: nat]: + induct [case_names Zero Suc, induct type: nat]: "P(0) ==> (!!x. P(x) ==> P(Suc(x))) ==> P(n)" Suc_inject: "Suc(m) = Suc(n) ==> m = n" Suc_neq_0: "Suc(m) = 0 ==> R"