# HG changeset patch
# User nipkow
# Date 864299152 -7200
# Node ID 8b143c196d42fa62f6ecea6973c76599391ac384
# Parent  cf322b5c59aa8f0763a17a10450b11da40f8ea81
Added rotation to exhaust_tac.

diff -r cf322b5c59aa -r 8b143c196d42 src/HOL/List.ML
--- a/src/HOL/List.ML	Thu May 22 12:59:08 1997 +0200
+++ b/src/HOL/List.ML	Thu May 22 13:05:52 1997 +0200
@@ -464,7 +464,7 @@
 by(exhaust_tac "n" 1);
  by(Blast_tac 1);
 by(exhaust_tac "i" 1);
-by(ALLGOALS (hyp_subst_tac THEN' Asm_full_simp_tac));
+by(ALLGOALS Asm_full_simp_tac);
 qed_spec_mp "nth_take";
 Addsimps [nth_take];
 
diff -r cf322b5c59aa -r 8b143c196d42 src/HOL/NatDef.ML
--- 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})];
 
 
diff -r cf322b5c59aa -r 8b143c196d42 src/HOL/datatype.ML
--- a/src/HOL/datatype.ML	Thu May 22 12:59:08 1997 +0200
+++ b/src/HOL/datatype.ML	Thu May 22 13:05:52 1997 +0200
@@ -5,6 +5,11 @@
    Copyright 1995 TU Muenchen
 *)
 
+(* should go into Pure *)
+fun ALLNEWSUBGOALS tac tacf i =
+  STATE (fn state0 => tac i THEN
+  STATE (fn state1 => let val d = nprems_of state1 - nprems_of state0
+                      in EVERY(map tacf ((i+d) downto i)) end));
 
 (*used for constructor parameters*)
 datatype dt_type = dtVar of string |
@@ -858,7 +863,9 @@
      val {nchotomy,case_cong} = case_thms sign case_rewrites itac
      val exhaustion = mk_exhaust nchotomy
      val exh_var = exhaust_var exhaustion;
-     fun exhaust_tac a = res_inst_tac [(exh_var,a)] exhaustion;
+     fun exhaust_tac a =
+           ALLNEWSUBGOALS (res_inst_tac [(exh_var,a)] exhaustion)
+                          (rotate_tac ~1);
      fun induct_tac a i =
            STATE(fn st =>
              (if Datatype.occs_in_prems a i st