# HG changeset patch
# User wenzelm
# Date 1213133315 -7200
# Node ID 63fdfcf6c7a3df6e2120356f5c518879d51129b2
# Parent  d0070c32fdc1b2b0f8f2114d609d930f11b3c6ab
proper deletion of nat cases/induct rules from type_definition;

diff -r d0070c32fdc1 -r 63fdfcf6c7a3 src/HOL/Word/TdThs.thy
--- a/src/HOL/Word/TdThs.thy	Tue Jun 10 21:50:30 2008 +0200
+++ b/src/HOL/Word/TdThs.thy	Tue Jun 10 23:28:35 2008 +0200
@@ -93,9 +93,11 @@
 interpretation nat_int: type_definition [int nat "Collect (op <= 0)"]
   by (rule td_nat_int)
 
-text "resetting to the default nat induct and cases rules"
-declare nat_induct [induct type: nat]
-declare nat.exhaust [cases type: nat]
+declare
+  nat_int.Rep_cases [cases del]
+  nat_int.Abs_cases [cases del]
+  nat_int.Rep_induct [induct del]
+  nat_int.Abs_induct [induct del]
 
 
 subsection "Extended form of type definition predicate"