induct: case names;
authorwenzelm
Fri Oct 05 21:42:10 2001 +0200 (2001-10-05)
changeset 11696233362cfecc7
parent 11695 8c66866fb0ff
child 11697 8dd899efbd35
induct: case names;
src/FOL/ex/Natural_Numbers.thy
     1.1 --- a/src/FOL/ex/Natural_Numbers.thy	Fri Oct 05 21:37:33 2001 +0200
     1.2 +++ b/src/FOL/ex/Natural_Numbers.thy	Fri Oct 05 21:42:10 2001 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
     1.5  
     1.6  axioms
     1.7 -  induct [induct type: nat]:
     1.8 +  induct [case_names Zero Suc, induct type: nat]:
     1.9      "P(0) ==> (!!x. P(x) ==> P(Suc(x))) ==> P(n)"
    1.10    Suc_inject: "Suc(m) = Suc(n) ==> m = n"
    1.11    Suc_neq_0: "Suc(m) = 0 ==> R"