# HG changeset patch
# User wenzelm
# Date 1213127377 -7200
# Node ID 7fa9fa0bcceeb60840741b4bfb70788e0f5a8ab2
# Parent  71461c77a15b7d18cb09611ba10448a72814ec78
more robust declaration of nat_induct;

diff -r 71461c77a15b -r 7fa9fa0bccee src/HOL/Word/TdThs.thy
--- a/src/HOL/Word/TdThs.thy	Tue Jun 10 21:49:11 2008 +0200
+++ b/src/HOL/Word/TdThs.thy	Tue Jun 10 21:49:37 2008 +0200
@@ -93,9 +93,9 @@
 interpretation nat_int: type_definition [int nat "Collect (op <= 0)"]
   by (rule td_nat_int)
 
--- "resetting to the default nat induct and cases rules"
-declare Nat.induct [case_names 0 Suc, induct type]
-declare Nat.exhaust [case_names 0 Suc, cases type]
+text "resetting to the default nat induct and cases rules"
+declare nat_induct [induct type: nat]
+declare nat.exhaust [cases type: nat]
 
 
 subsection "Extended form of type definition predicate"