# HG changeset patch
# User wenzelm
# Date 1003185053 -7200
# Node ID da81334357bae62e06b3a7606da092ecdd50e7c2
# Parent  60054fee3c16b9f692add2730eacd38d3c3e9612
tuned;

diff -r 60054fee3c16 -r da81334357ba src/FOL/ex/Natural_Numbers.thy
--- a/src/FOL/ex/Natural_Numbers.thy	Mon Oct 15 21:04:46 2001 +0200
+++ b/src/FOL/ex/Natural_Numbers.thy	Tue Oct 16 00:30:53 2001 +0200
@@ -17,7 +17,7 @@
   rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
 
 axioms
-  induct [case_names Zero Suc, induct type: nat]:
+  induct [case_names 0 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"