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