# HG changeset patch
# User wenzelm
# Date 878587941 -3600
# Node ID 84433b1ab8262f424ed4257c0dd15145ff70651c
# Parent  884968ad30da5a6bab4e3df9b79a127319f9dc7b
nat datatype_info moved to Nat.thy;

diff -r 884968ad30da -r 84433b1ab826 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Nov 03 21:04:51 1997 +0100
+++ b/src/HOL/Nat.thy	Mon Nov 03 21:12:21 1997 +0100
@@ -8,6 +8,20 @@
 
 Nat = NatDef +
 
+(*install 'automatic' induction tactic, pretending nat is a datatype
+  except for induct_tac and exhaust_tac, everything is dummy*)
+
+MLtext {|
+|> Dtype.add_datatype_info
+("nat", {case_const = Bound 0, case_rewrites = [],
+  constructors = [], induct_tac = nat_ind_tac,
+  exhaustion = natE,
+  exhaust_tac = fn v => ALLNEWSUBGOALS (res_inst_tac [("n",v)] natE)
+                                       (rotate_tac ~1),
+  nchotomy = ProtoPure.flexpair_def, case_cong = ProtoPure.flexpair_def})
+|}
+
+
 instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
 
 consts
diff -r 884968ad30da -r 84433b1ab826 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Mon Nov 03 21:04:51 1997 +0100
+++ b/src/HOL/NatDef.ML	Mon Nov 03 21:12:21 1997 +0100
@@ -70,15 +70,6 @@
 by (Blast_tac 1);
 qed "natE";
 
-(*Install 'automatic' induction tactic, pretending nat is a datatype *)
-(*except for induct_tac and exhaust_tac, everything is dummy*)
-datatypes := [("nat",{case_const = Bound 0, case_rewrites = [],
-  constructors = [], induct_tac = nat_ind_tac,
-  exhaustion = natE,
-  exhaust_tac = fn v => ALLNEWSUBGOALS (res_inst_tac [("n",v)] natE)
-                                       (rotate_tac ~1),
-  nchotomy = ProtoPure.flexpair_def, case_cong = ProtoPure.flexpair_def})];
-
 
 (*** Isomorphisms: Abs_Nat and Rep_Nat ***)