--- a/src/HOL/NatDef.ML Thu May 22 12:59:08 1997 +0200
+++ b/src/HOL/NatDef.ML Thu May 22 13:05:52 1997 +0200
@@ -70,10 +70,12 @@
qed "natE";
(*Install 'automatic' induction tactic, pretending nat is a datatype *)
-(*except for induct_tac, everything is dummy*)
+(*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 => res_inst_tac [("n",v)] natE,
+ exhaustion = natE,
+ exhaust_tac = fn v => ALLNEWSUBGOALS (res_inst_tac [("n",v)] natE)
+ (rotate_tac ~1),
nchotomy = flexpair_def, case_cong = flexpair_def})];