--- 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
--- 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 ***)