--- a/src/HOL/NatDef.ML Wed May 21 17:31:12 1997 +0200
+++ b/src/HOL/NatDef.ML Thu May 22 09:20:28 1997 +0200
@@ -46,13 +46,6 @@
COND (Datatype.occs_in_prems a (i+1)) all_tac
(rename_last_tac a [""] (i+1))];
-(*Install 'automatic' induction tactic, pretending nat is a datatype *)
-(*except for induct_tac, everything is dummy*)
-datatypes := [("nat",{case_const = Bound 0, case_rewrites = [],
- constructors = [], induct_tac = nat_ind_tac,
- nchotomy = flexpair_def, case_cong = flexpair_def})];
-
-
(*A special form of induction for reasoning about m<n and m-n*)
val prems = goal thy
"[| !!x. P x 0; \
@@ -76,6 +69,14 @@
by (Blast_tac 1);
qed "natE";
+(*Install 'automatic' induction tactic, pretending nat is a datatype *)
+(*except for induct_tac, everything is dummy*)
+datatypes := [("nat",{case_const = Bound 0, case_rewrites = [],
+ constructors = [], induct_tac = nat_ind_tac,
+ exhaustion = natE, exhaust_tac = fn v => res_inst_tac [("n",v)] natE,
+ nchotomy = flexpair_def, case_cong = flexpair_def})];
+
+
(*** Isomorphisms: Abs_Nat and Rep_Nat ***)
(*We can't take these properties as axioms, or take Abs_Nat==Inv(Rep_Nat),