# HG changeset patch
# User nipkow
# Date 952948270 -3600
# Node ID 3c19160b6432ea32839cdea1c8d546f3fdd7ef64
# Parent  6c6a5410a9bdb86a5394fdf652b85c0625e88afa
exhaust_tac -> cases_tac

diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Arith.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -106,24 +106,24 @@
 (** Reasoning about m+0=0, etc. **)
 
 Goal "(m+n = 0) = (m=0 & n=0)";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
 by (Auto_tac);
 qed "add_is_0";
 AddIffs [add_is_0];
 
 Goal "(0 = m+n) = (m=0 & n=0)";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
 by (Auto_tac);
 qed "zero_is_add";
 AddIffs [zero_is_add];
 
 Goal "(m+n=1) = (m=1 & n=0 | m=0 & n=1)";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
 by (Auto_tac);
 qed "add_is_1";
 
 Goal "(1=m+n) = (m=1 & n=0 | m=0 & n=1)";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
 by (Auto_tac);
 qed "one_is_add";
 
@@ -134,7 +134,7 @@
 
 (* Could be generalized, eg to "k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
 Goal "0<n ==> m + (n-1) = (m+n)-1";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc, Suc_n_not_n]
                                       addsplits [nat.split])));
 qed "add_pred";
@@ -404,7 +404,7 @@
 Addsimps [Suc_diff_diff];
 
 Goal "0<n ==> n - Suc i < n";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
 by Safe_tac;
 by (asm_simp_tac (simpset() addsimps le_simps) 1);
 qed "diff_Suc_less";
@@ -1161,16 +1161,16 @@
 (** Lemmas for ex/Factorization **)
 
 Goal "[| 1<n; 1<m |] ==> 1<m*n";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
 by Auto_tac;
 qed "one_less_mult"; 
 
 Goal "[| 1<n; 1<m |] ==> n<m*n";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
 by Auto_tac;
 qed "n_less_m_mult_n"; 
 
 Goal "[| 1<n; 1<m |] ==> n<n*m";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
 by Auto_tac;
 qed "n_less_n_mult_m"; 
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/BCV/DFAimpl.ML
--- a/src/HOL/BCV/DFAimpl.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/BCV/DFAimpl.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -60,7 +60,7 @@
      by (Force_tac 2);
     by (assume_tac 2);
    by (assume_tac 2);
-  by (exhaust_tac "xs!p" 1);
+  by (cases_tac "xs!p" 1);
    by (asm_full_simp_tac (simpset() addsimps [list_update_le_conv]) 1);
   by (asm_full_simp_tac (simpset() addsimps
       [list_update_le_conv,listsn_optionE_in]) 1);
@@ -147,7 +147,7 @@
 \         step p s = Some(t) & merges t (succs p) sos = sos))";
 by (rtac iffI 1);
  by (asm_simp_tac (simpset() addsimps [next_Some1]) 1);
-by (exhaust_tac "next step succs sos" 1);
+by (cases_tac "next step succs sos" 1);
  by (best_tac (claset() addSDs [next_None] addss simpset()) 1);
 by (rename_tac "sos'" 1);
 by (case_tac "sos' = sos" 1);
@@ -172,7 +172,7 @@
 \    step_pres_type step n A; succs_bounded succs n;\
 \    sos : listsn n (option A) |] ==> \
 \ next step succs sos : option (listsn n (option A))";
-by (exhaust_tac "next step succs sos" 1);
+by (cases_tac "next step succs sos" 1);
  by (ALLGOALS Asm_simp_tac);
 by (rename_tac "sos'" 1);
 by (case_tac "sos' = sos" 1);
@@ -256,7 +256,7 @@
 by (subgoal_tac
    "!p<n. !s. sos!p = Some s --> (? u. \
 \             step p s = Some(u) & (!q:set(succs p). Some u<=tos!q))" 1);
- by (exhaust_tac "next step succs sos" 1);
+ by (cases_tac "next step succs sos" 1);
   by (dtac next_None 1);
      by (assume_tac 1);
     by (assume_tac 1);
@@ -279,12 +279,12 @@
     by (blast_tac (claset() addIs [succs_boundedD,listsn_optionE_in]) 1);
    by (REPEAT(atac 1));
 by (Clarify_tac 1);
-by (exhaust_tac "tos!p" 1);
+by (cases_tac "tos!p" 1);
  by (force_tac (claset() addDs [le_listD],simpset()) 1);
 by (rename_tac "t" 1);
 by (subgoal_tac "s <= t" 1);
  by (force_tac (claset() addDs [le_listD],simpset()) 2);
-by (exhaust_tac "step p s" 1);
+by (cases_tac "step p s" 1);
  by (dtac step_mono_NoneD 1);
      by (assume_tac 4);
     by (blast_tac (claset() addIs [listsn_optionE_in]) 1);
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/BCV/Machine.ML
--- a/src/HOL/BCV/Machine.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/BCV/Machine.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -68,15 +68,15 @@
 by (Blast_tac 2);
 by (etac thin_rl 1);
 by (asm_full_simp_tac (simpset() addsimps [le_typ])1);
-by (exhaust_tac "t!nat1" 1);
+by (cases_tac "t!nat1" 1);
 by (ALLGOALS Asm_full_simp_tac);
-by (exhaust_tac "t!nat2" 1);
+by (cases_tac "t!nat2" 1);
 by (ALLGOALS Asm_full_simp_tac);
-by (exhaust_tac "t!nat2" 1);
+by (cases_tac "t!nat2" 1);
 by (ALLGOALS Asm_full_simp_tac);
-by (exhaust_tac "s!nat1" 1);
+by (cases_tac "s!nat1" 1);
 by (ALLGOALS Asm_full_simp_tac);
-by (exhaust_tac "t!nat2" 1);
+by (cases_tac "t!nat2" 1);
 by (ALLGOALS Asm_full_simp_tac);
 
 qed "exec_mono_None";
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/BCV/Orders.ML
--- a/src/HOL/BCV/Orders.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/BCV/Orders.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -37,7 +37,7 @@
 by (case_tac "? a. Some a : Q" 1);
  by (eres_inst_tac [("x","{a . Some a : Q}")] allE 1);
  by (Blast_tac 1);
-by (exhaust_tac "x" 1);
+by (cases_tac "x" 1);
  by (Fast_tac 1);
 by (Blast_tac 1);
 qed "acc_option";
@@ -70,18 +70,18 @@
  by (Asm_full_simp_tac 1);
 by (Asm_full_simp_tac 1);
 by (Clarify_tac 1);
-by (exhaust_tac "i" 1);
+by (cases_tac "i" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "Cons_le_Cons";
 AddIffs [Cons_le_Cons];
 
 Goal "(x#xs <= ys) = (? z zs. ys = z#zs & x <= z & xs <= zs)";
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "Cons_le_iff";
 
 Goal "(xs <= y#ys) = (? z zs. xs = z#zs & z <= y & zs <= ys)";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "le_Cons_iff";
 
@@ -120,7 +120,7 @@
 
 Goalw [listsn_def]
  "(xs : listsn (Suc n) A) = (? y:A. ? ys:listsn n A. xs = y#ys)";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
 by (Auto_tac);
 qed "in_listsn_Suc_iff";
 
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/BCV/Orders0.ML
--- a/src/HOL/BCV/Orders0.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/BCV/Orders0.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -58,11 +58,11 @@
 by (induct_tac "xs" 1);
  by (Simp_tac 1);
 by (rtac allI 1);
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
  by (hyp_subst_tac 1);
  by (Simp_tac 1);
 by (rtac allI 1);
-by (exhaust_tac "zs" 1);
+by (cases_tac "zs" 1);
  by (hyp_subst_tac 1);
  by (Simp_tac 1);
 by (hyp_subst_tac 1);
@@ -87,7 +87,7 @@
 by (induct_tac "xs" 1);
  by (Simp_tac 1);
 by (rtac allI 1);
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
  by (hyp_subst_tac 1);
  by (Simp_tac 1);
 by (hyp_subst_tac 1);
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/BCV/SemiLattice.ML
--- a/src/HOL/BCV/SemiLattice.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/BCV/SemiLattice.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -87,9 +87,9 @@
 by (induct_tac "n" 1);
  by (Simp_tac 1);
 by (Clarify_tac 1);
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
  by (Asm_full_simp_tac 1);
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
  by (Asm_full_simp_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1);
 qed_spec_mp "nth_plus";
@@ -123,9 +123,9 @@
  by (Simp_tac 1);
 by (Asm_full_simp_tac 1);
 by (Clarify_tac 1);
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
  by (Asm_full_simp_tac 1);
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
  by (Asm_full_simp_tac 1);
 by (Asm_full_simp_tac 1);
 by (blast_tac (claset() addIs [semilat_plus]) 1);
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/BCV/Types0.ML
--- a/src/HOL/BCV/Types0.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/BCV/Types0.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -23,7 +23,7 @@
 Goal "(UNIV::typ set) = {Atyp,Btyp,Ctyp,Top}";
 by (Auto_tac);
 by (rename_tac "t" 1);
-by (exhaust_tac "t" 1);
+by (cases_tac "t" 1);
 by (Auto_tac);
 qed "UNIV_typ_enum";
 
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Finite.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -248,7 +248,7 @@
 
 Goal "[| x ~: A; insert x A = {f i|i. i<n} |]  \
 \     ==> ? m::nat. m<n & (? g. A = {g i|i. i<m})";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
  by (hyp_subst_tac 1);
  by (Asm_full_simp_tac 1);
 by (rename_tac "m" 1);
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/Hoare/Examples.ML
--- a/src/HOL/Hoare/Examples.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Hoare/Examples.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -50,7 +50,7 @@
 \ OD \
 \ {c = A^B}";
 by (hoare_tac (Asm_full_simp_tac) 1);
-by (exhaust_tac "b" 1);
+by (cases_tac "b" 1);
 by (hyp_subst_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [mod_less]) 1);
 by (asm_simp_tac (simpset() addsimps [mult_assoc]) 1);
@@ -67,7 +67,7 @@
 \ {b = fac A}";
 by (hoare_tac Asm_full_simp_tac 1);
 by (Clarify_tac 1);
-by (exhaust_tac "a" 1);
+by (cases_tac "a" 1);
 by (ALLGOALS
     (asm_simp_tac
      (simpset() addsimps [add_mult_distrib,add_mult_distrib2,mult_assoc])));
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/IMP/Transition.ML
--- a/src/HOL/IMP/Transition.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/IMP/Transition.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -220,7 +220,7 @@
 by (Clarify_tac 1);
 by (etac rel_pow_E2 1);
  by (asm_full_simp_tac (simpset() addsimps evalc.intrs) 1);
-by (exhaust_tac "c" 1);
+by (cases_tac "c" 1);
     by (fast_tac (claset() addSDs [hlemma]) 1);
    by (Blast_tac 1);
   by (blast_tac (claset() addSDs [rel_pow_Suc_I2 RS comp_decomp_lemma]) 1);
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/IOA/IOA.ML
--- a/src/HOL/IOA/IOA.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/IOA/IOA.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -30,7 +30,7 @@
 Goal "filter_oseq p (filter_oseq p s) = filter_oseq p s";
   by (simp_tac (simpset() addsimps [filter_oseq_def]) 1);
   by (rtac ext 1);
-  by (exhaust_tac "s(i)" 1);
+  by (cases_tac "s(i)" 1);
   by (Asm_simp_tac 1);
   by (Asm_simp_tac 1);
 qed "filter_oseq_idemp";
@@ -41,7 +41,7 @@
 \  &                                                              \
 \  (mk_trace A s n = Some(a)) =                                   \
 \   (s(n)=Some(a) & a : externals(asig_of(A)))";
-  by (exhaust_tac "s(n)" 1);
+  by (cases_tac "s(n)" 1);
   by (ALLGOALS Asm_simp_tac);
   by (Fast_tac 1);
 qed "mk_trace_thm";
@@ -86,7 +86,7 @@
   by (induct_tac "n" 1);
    by (fast_tac (claset() addIs [p1,reachable_0]) 1);
   by (eres_inst_tac[("x","na")] allE 1);
-  by (exhaust_tac "ex1 na" 1 THEN ALLGOALS Asm_full_simp_tac);
+  by (cases_tac "ex1 na" 1 THEN ALLGOALS Asm_full_simp_tac);
   by Safe_tac;
    by (etac (p2 RS mp) 1);
     by (ALLGOALS(fast_tac(claset() addDs [reachable_n])));
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/Induct/LList.ML
--- a/src/HOL/Induct/LList.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Induct/LList.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -76,7 +76,7 @@
     "LList_corec a f <= \
 \    (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))";
 by (rtac UN_least 1);
-by (exhaust_tac "k" 1);
+by (cases_tac "k" 1);
 by (ALLGOALS Asm_simp_tac);
 by (REPEAT (resolve_tac [allI, impI, subset_refl RS CONS_mono, 
 			 UNIV_I RS UN_upper] 1));
@@ -132,10 +132,10 @@
 by (safe_tac (claset() delrules [equalityI]));
 by (etac LListD.elim 1);
 by (safe_tac (claset() delrules [equalityI]));
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
 by (Asm_simp_tac 1);
 by (rename_tac "n'" 1);
-by (exhaust_tac "n'" 1);
+by (cases_tac "n'" 1);
 by (asm_simp_tac (simpset() addsimps [CONS_def]) 1);
 by (asm_simp_tac (simpset() addsimps [CONS_def, less_Suc_eq]) 1);
 qed "LListD_implies_ntrunc_equality";
@@ -295,9 +295,9 @@
 by (stac prem2 1);
 by (Simp_tac 1);
 by (strip_tac 1);
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
 by (rename_tac "m" 2);
-by (exhaust_tac "m" 2);
+by (cases_tac "m" 2);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
 result();
 
@@ -598,7 +598,7 @@
     "llist_corec a f =  \
 \    (case f a of None => LNil | Some(z,w) => LCons z (llist_corec w f))";
 by (stac LList_corec 1);
-by (exhaust_tac "f a" 1);
+by (cases_tac "f a" 1);
 by (asm_simp_tac (simpset() addsimps [LList_corec_type2]) 1);
 by (force_tac (claset(), simpset() addsimps [LList_corec_type2]) 1);
 qed "llist_corec";
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/Integ/Int.ML
--- a/src/HOL/Integ/Int.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Integ/Int.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -90,7 +90,7 @@
 by (cut_inst_tac [("m","m")] int_Suc_int_1 1);
 by (cut_inst_tac [("m","n")] int_Suc_int_1 1);
 by (Asm_full_simp_tac 1);
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
 by Auto_tac;
 by (cut_inst_tac [("m","m")] int_Suc_int_1 1);
 by (full_simp_tac (simpset() addsimps zadd_ac) 1);
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/Integ/NatBin.ML
--- a/src/HOL/Integ/NatBin.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Integ/NatBin.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -319,17 +319,17 @@
 (* These two can be useful when m = number_of... *)
 
 Goal "(m::nat) + n = (if m=#0 then n else Suc ((m - #1) + n))";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
 by (ALLGOALS (asm_simp_tac numeral_ss));
 qed "add_eq_if";
 
 Goal "(m::nat) * n = (if m=#0 then #0 else n + ((m - #1) * n))";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
 by (ALLGOALS (asm_simp_tac numeral_ss));
 qed "mult_eq_if";
 
 Goal "(p ^ m :: nat) = (if m=#0 then #1 else p * (p ^ (m - #1)))";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
 by (ALLGOALS (asm_simp_tac numeral_ss));
 qed "power_eq_if";
 
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/Lambda/Eta.ML
--- a/src/HOL/Lambda/Eta.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Lambda/Eta.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -166,7 +166,7 @@
   by (rtac notE 1);
    by (assume_tac 2);
   by (etac thin_rl 1);
-  by (exhaust_tac "t" 1);
+  by (cases_tac "t" 1);
     by (Asm_simp_tac 1);
    by (Asm_simp_tac 1);
   by (Asm_simp_tac 1);
@@ -181,7 +181,7 @@
   by (Asm_simp_tac 1);
  by (etac exE 1);
  by (etac rev_mp 1);
- by (exhaust_tac "t" 1);
+ by (cases_tac "t" 1);
    by (Asm_simp_tac 1);
   by (Asm_simp_tac 1);
   by (Blast_tac 1);
@@ -195,7 +195,7 @@
  by (Asm_simp_tac 1);
 by (etac exE 1);
 by (etac rev_mp 1);
-by (exhaust_tac "t" 1);
+by (cases_tac "t" 1);
   by (Asm_simp_tac 1);
  by (Asm_simp_tac 1);
 by (Asm_simp_tac 1);
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/Lambda/InductTermi.ML
--- a/src/HOL/Lambda/InductTermi.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Lambda/InductTermi.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -86,7 +86,7 @@
   by (eres_inst_tac [("x","Var n $$ us")] allE 1);
   by (Force_tac 1);
 by (rename_tac "u ts" 1);
-by (exhaust_tac "ts" 1);
+by (cases_tac "ts" 1);
  by (Asm_full_simp_tac 1);
  by (blast_tac (claset() addIs IT.intrs) 1);
 by (rename_tac "s ss" 1);
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/Lambda/ListBeta.ML
--- a/src/HOL/Lambda/ListBeta.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Lambda/ListBeta.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -29,7 +29,7 @@
 \       (? s t ts. r = Abs s & rs = t#ts & u' = s[t/0]$$ts))";
 by (etac beta.induct 1);
    by (clarify_tac (claset() delrules [disjCI]) 1);
-   by (exhaust_tac "r" 1);
+   by (cases_tac "r" 1);
      by (Asm_full_simp_tac 1);
     by (asm_full_simp_tac (simpset() addsimps [App_eq_foldl_conv]) 1);
     by (split_asm_tac [split_if_asm] 1);
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/Lambda/ListOrder.ML
--- a/src/HOL/Lambda/ListOrder.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Lambda/ListOrder.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -30,7 +30,7 @@
 by (rtac iffI 1);
  by (etac exE 1);
  by (rename_tac "ts" 1);
- by (exhaust_tac "ts" 1);
+ by (cases_tac "ts" 1);
   by (Force_tac 1);
  by (Force_tac 1);
 by (etac disjE 1);
@@ -51,7 +51,7 @@
 \        !y. ys = y#xs --> (y,x) : r --> R; \
 \        !zs. ys = x#zs --> (zs,xs) : step1 r --> R \
 \     |] ==> R";
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
  by (asm_full_simp_tac (simpset() addsimps [step1_def]) 1);
 by (Blast_tac 1);
 val lemma = result();
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/Lex/MaxPrefix.ML
--- a/src/HOL/Lex/MaxPrefix.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Lex/MaxPrefix.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -26,7 +26,7 @@
 by (case_tac "? us. us <= a#list & P (ps @ us)" 1);
  by (Asm_simp_tac 1);
  by (Clarify_tac 1);
- by (exhaust_tac "us" 1);
+ by (cases_tac "us" 1);
   by (rtac iffI 1);
    by (asm_full_simp_tac (simpset() addsimps [prefix_Cons,prefix_append]) 1);
    by (Blast_tac 1);
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/Lex/NAe.ML
--- a/src/HOL/Lex/NAe.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Lex/NAe.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -5,7 +5,7 @@
 *)
 
 Goal "steps A w O (eps A)^* = steps A w";
-by (exhaust_tac "w" 1);
+by (cases_tac "w" 1);
 by (ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
 qed_spec_mp "steps_epsclosure";
 Addsimps [steps_epsclosure];
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/Lex/Prefix.ML
--- a/src/HOL/Lex/Prefix.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Lex/Prefix.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -76,7 +76,7 @@
 
 Goalw [prefix_def]
    "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
 by Auto_tac;
 qed "prefix_Cons";
 
@@ -92,7 +92,7 @@
 Goalw [prefix_def]
   "[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys";
 by (auto_tac(claset(), simpset() addsimps [nth_append]));
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
 by Auto_tac;
 qed "append_one_prefix";
 
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/Lex/RegExp2NA.ML
--- a/src/HOL/Lex/RegExp2NA.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Lex/RegExp2NA.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -112,7 +112,7 @@
 \ ( (w = [] & q = start(union L R)) | \
 \   (w ~= [] & (? p.  q = True  # p & (start L,p) : steps L w | \
 \                     q = False # p & (start R,p) : steps R w)))";
-by (exhaust_tac "w" 1);
+by (cases_tac "w" 1);
  by (Asm_simp_tac 1);
  by (Blast_tac 1);
 by (Asm_simp_tac 1);
@@ -273,7 +273,7 @@
  by (Simp_tac 1);
  by (Blast_tac 1);
 by (Clarify_tac 1);
-by (exhaust_tac "v" 1);
+by (cases_tac "v" 1);
  by (Asm_full_simp_tac 1);
  by (Blast_tac 1);
 by (Asm_full_simp_tac 1);
@@ -336,7 +336,7 @@
 Goal
  "[| (start A,q) : steps A u; u ~= []; fin A p |] \
 \ ==> (p,q) : steps (plus A) u";
-by (exhaust_tac "u" 1);
+by (cases_tac "u" 1);
  by (Blast_tac 1);
 by (Asm_full_simp_tac 1);
 by (blast_tac (claset() addIs [steps_plusI]) 1);
@@ -360,7 +360,7 @@
  by (res_inst_tac [("x","us")] exI 1);
  by (Asm_simp_tac 1);
  by (Blast_tac 1);
-by (exhaust_tac "v" 1);
+by (cases_tac "v" 1);
  by (res_inst_tac [("x","us")] exI 1);
  by (Asm_full_simp_tac 1);
 by (res_inst_tac [("x","us@[v]")] exI 1);
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/Lex/RegExp2NAe.ML
--- a/src/HOL/Lex/RegExp2NAe.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Lex/RegExp2NAe.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -191,7 +191,7 @@
 \ ( (w = [] & q = start(union L R)) | \
 \   (? p.  q = True  # p & (start L,p) : steps L w | \
 \          q = False # p & (start R,p) : steps R w) )";
-by (exhaust_tac "w" 1);
+by (cases_tac "w" 1);
  by (Asm_simp_tac 1);
  by (Blast_tac 1);
 by (Asm_simp_tac 1);
@@ -568,7 +568,7 @@
  "(start(star A),r) : steps (star A) w = \
 \ ((w=[] & r= start(star A)) | (True#start A,r) : steps (star A) w)";
 by (rtac iffI 1);
- by (exhaust_tac "w" 1);
+ by (cases_tac "w" 1);
   by (asm_full_simp_tac (simpset() addsimps
     [epsclosure_start_step_star]) 1);
  by (Asm_full_simp_tac 1);
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/Lex/RegSet_of_nat_DA.ML
--- a/src/HOL/Lex/RegSet_of_nat_DA.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Lex/RegSet_of_nat_DA.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -11,7 +11,7 @@
 (* Lists *)
 
 Goal "(butlast xs = []) = (case xs of [] => True | y#ys => ys=[])";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "butlast_empty";
 AddIffs [butlast_empty];
@@ -103,14 +103,14 @@
 Addsimps [trace_concat];
 
 Goal "!i. (trace d i xs = []) = (xs = [])";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "trace_is_Nil";
 Addsimps [trace_is_Nil];
 
 Goal "(trace d i xs = n#ns) = \
 \         (case xs of [] => False | y#ys => n = d y i & ns = trace d n ys)";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 by (Blast_tac 1);
 qed_spec_mp "trace_is_Cons_conv";
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/List.ML
--- a/src/HOL/List.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/List.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -88,7 +88,7 @@
 Addsimps [length_rev];
 
 Goal "length(tl xs) = (length xs) - 1";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
 by Auto_tac;
 qed "length_tl";
 Addsimps [length_tl];
@@ -159,11 +159,11 @@
 \              --> (xs@us = ys@vs) = (xs=ys & us=vs)";
 by (induct_tac "xs" 1);
  by (rtac allI 1);
- by (exhaust_tac "ys" 1);
+ by (cases_tac "ys" 1);
   by (Asm_simp_tac 1);
  by (Force_tac 1);
 by (rtac allI 1);
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
 by (Force_tac 1);
 by (Asm_simp_tac 1);
 qed_spec_mp "append_eq_append_conv";
@@ -340,19 +340,19 @@
 bind_thm("map_cong", impI RSN (2,allI RSN (2, result() RS mp)));
 
 Goal "(map f xs = []) = (xs = [])";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
 by Auto_tac;
 qed "map_is_Nil_conv";
 AddIffs [map_is_Nil_conv];
 
 Goal "([] = map f xs) = (xs = [])";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
 by Auto_tac;
 qed "Nil_is_map_conv";
 AddIffs [Nil_is_map_conv];
 
 Goal "(map f xs = y#ys) = (? x xs'. xs = x#xs' & f x = y & map f xs' = ys)";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "map_eq_Cons";
 
@@ -411,7 +411,7 @@
 by (induct_tac "xs" 1);
  by (Force_tac 1);
 by (rtac allI 1);
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
  by (Asm_simp_tac 1);
 by (Force_tac 1);
 qed_spec_mp "rev_is_rev_conv";
@@ -492,7 +492,7 @@
 by (rtac iffI 1);
 by (blast_tac (claset() addIs [eq_Nil_appendI,Cons_eq_appendI]) 1);
 by (REPEAT(etac exE 1));
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
 by Auto_tac;
 qed "in_set_conv_decomp";
 
@@ -630,7 +630,7 @@
 by (induct_tac "xs" 1);
  by (Asm_simp_tac 1);
  by (rtac allI 1);
- by (exhaust_tac "n" 1);
+ by (cases_tac "n" 1);
   by Auto_tac;
 qed_spec_mp "nth_append";
 
@@ -652,7 +652,7 @@
   by (Simp_tac 1);
  by (res_inst_tac [("x","Suc i")] exI 1);
  by (Asm_simp_tac 1);
-by (exhaust_tac "i" 1);
+by (cases_tac "i" 1);
  by (Asm_full_simp_tac 1);
 by (rename_tac "j" 1);
  by (res_inst_tac [("x","j")] exI 1);
@@ -728,7 +728,7 @@
 \     (zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])";
 by (induct_tac "ys" 1);
  by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
  by (auto_tac (claset(), simpset() addsplits [nat.split]));
 qed_spec_mp "update_zip";
 
@@ -813,7 +813,7 @@
 Goal "!xs. length(take n xs) = min (length xs) n";
 by (induct_tac "n" 1);
  by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
  by Auto_tac;
 qed_spec_mp "length_take";
 Addsimps [length_take];
@@ -821,7 +821,7 @@
 Goal "!xs. length(drop n xs) = (length xs - n)";
 by (induct_tac "n" 1);
  by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
  by Auto_tac;
 qed_spec_mp "length_drop";
 Addsimps [length_drop];
@@ -829,7 +829,7 @@
 Goal "!xs. length xs <= n --> take n xs = xs";
 by (induct_tac "n" 1);
  by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
  by Auto_tac;
 qed_spec_mp "take_all";
 Addsimps [take_all];
@@ -837,7 +837,7 @@
 Goal "!xs. length xs <= n --> drop n xs = []";
 by (induct_tac "n" 1);
  by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
  by Auto_tac;
 qed_spec_mp "drop_all";
 Addsimps [drop_all];
@@ -845,7 +845,7 @@
 Goal "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
 by (induct_tac "n" 1);
  by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
  by Auto_tac;
 qed_spec_mp "take_append";
 Addsimps [take_append];
@@ -853,7 +853,7 @@
 Goal "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys"; 
 by (induct_tac "n" 1);
  by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
  by Auto_tac;
 qed_spec_mp "drop_append";
 Addsimps [drop_append];
@@ -861,9 +861,9 @@
 Goal "!xs n. take n (take m xs) = take (min n m) xs"; 
 by (induct_tac "m" 1);
  by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
  by Auto_tac;
-by (exhaust_tac "na" 1);
+by (cases_tac "na" 1);
  by Auto_tac;
 qed_spec_mp "take_take";
 Addsimps [take_take];
@@ -871,7 +871,7 @@
 Goal "!xs. drop n (drop m xs) = drop (n + m) xs"; 
 by (induct_tac "m" 1);
  by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
  by Auto_tac;
 qed_spec_mp "drop_drop";
 Addsimps [drop_drop];
@@ -879,14 +879,14 @@
 Goal "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; 
 by (induct_tac "m" 1);
  by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
  by Auto_tac;
 qed_spec_mp "take_drop";
 
 Goal "!xs. take n xs @ drop n xs = xs";
 by (induct_tac "n" 1);
  by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
  by Auto_tac;
 qed_spec_mp "append_take_drop_id";
 Addsimps [append_take_drop_id];
@@ -894,23 +894,23 @@
 Goal "!xs. take n (map f xs) = map f (take n xs)"; 
 by (induct_tac "n" 1);
  by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
  by Auto_tac;
 qed_spec_mp "take_map"; 
 
 Goal "!xs. drop n (map f xs) = map f (drop n xs)"; 
 by (induct_tac "n" 1);
  by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
  by Auto_tac;
 qed_spec_mp "drop_map";
 
 Goal "!n i. i < n --> (take n xs)!i = xs!i";
 by (induct_tac "xs" 1);
  by Auto_tac;
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
  by (Blast_tac 1);
-by (exhaust_tac "i" 1);
+by (cases_tac "i" 1);
  by Auto_tac;
 qed_spec_mp "nth_take";
 Addsimps [nth_take];
@@ -918,7 +918,7 @@
 Goal  "!xs i. n + i <= length xs --> (drop n xs)!i = xs!(n+i)";
 by (induct_tac "n" 1);
  by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
  by Auto_tac;
 qed_spec_mp "nth_drop";
 Addsimps [nth_drop];
@@ -930,7 +930,7 @@
  by (Simp_tac 1);
 by (Asm_full_simp_tac 1);
 by (Clarify_tac 1);
-by (exhaust_tac "zs" 1);
+by (cases_tac "zs" 1);
 by (Auto_tac);
 qed_spec_mp "append_eq_conv_conj";
 
@@ -993,7 +993,7 @@
 by (induct_tac "ys" 1);
  by (Simp_tac 1);
 by (Clarify_tac 1);
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
  by (Auto_tac);
 qed_spec_mp "length_zip";
 Addsimps [length_zip];
@@ -1004,7 +1004,7 @@
 by (induct_tac "zs" 1);
  by (Simp_tac 1);
 by (Clarify_tac 1);
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
  by (Asm_simp_tac 1);
 by (Asm_simp_tac 1);
 qed_spec_mp "zip_append1";
@@ -1015,7 +1015,7 @@
 by (induct_tac "xs" 1);
  by (Simp_tac 1);
 by (Clarify_tac 1);
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
  by (Asm_simp_tac 1);
 by (Asm_simp_tac 1);
 qed_spec_mp "zip_append2";
@@ -1032,7 +1032,7 @@
  by (Asm_full_simp_tac 1);
 by (Asm_full_simp_tac 1);
 by (Clarify_tac 1);
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
  by (Auto_tac);
 qed_spec_mp "zip_rev";
 
@@ -1042,7 +1042,7 @@
 by (induct_tac "ys" 1);
  by (Simp_tac 1);
 by (Clarify_tac 1);
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
  by (Auto_tac);
 by (asm_full_simp_tac (simpset() addsimps (thms"nth.simps") addsplits [nat.split]) 1);
 qed_spec_mp "nth_zip";
@@ -1061,7 +1061,7 @@
 Goal "!j. zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)";
 by (induct_tac "i" 1);
  by (Auto_tac);
-by (exhaust_tac "j" 1);
+by (cases_tac "j" 1);
  by (Auto_tac);
 qed "zip_replicate";
 Addsimps [zip_replicate];
@@ -1091,13 +1091,13 @@
 
 Goalw [list_all2_def]
  "list_all2 P (x#xs) ys = (? z zs. ys = z#zs & P x z & list_all2 P xs zs)";
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
 by (Auto_tac);
 qed "list_all2_Cons1";
 
 Goalw [list_all2_def]
  "list_all2 P xs (y#ys) = (? z zs. xs = z#zs & P z y & list_all2 P zs ys)";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
 by (Auto_tac);
 qed "list_all2_Cons2";
 
@@ -1249,8 +1249,8 @@
 						all_conj_distrib])));
 by (Clarify_tac 1);
 (*Both lists must be non-empty*)
-by (exhaust_tac "xs" 1);
-by (exhaust_tac "ys" 2);
+by (cases_tac "xs" 1);
+by (cases_tac "ys" 2);
 by (ALLGOALS Clarify_tac);
 (*prenexing's needed, not miniscoping*)
 by (ALLGOALS (full_simp_tac (simpset() addsimps (all_simps RL [sym])  
@@ -1412,7 +1412,7 @@
  by (rename_tac "a xys x xs' y ys'" 1);
  by (res_inst_tac [("x","a#xys")] exI 1);
  by (Simp_tac 1);
-by (exhaust_tac "xys" 1);
+by (cases_tac "xys" 1);
  by (ALLGOALS (asm_full_simp_tac (simpset())));
 by (Blast_tac 1);
 qed "lexn_conv";
@@ -1452,7 +1452,7 @@
 by (rtac iffI 1);
  by (blast_tac (claset() addIs [Cons_eq_appendI]) 2);
 by (REPEAT(eresolve_tac [conjE, exE] 1));
-by (exhaust_tac "xys" 1);
+by (cases_tac "xys" 1);
 by (Asm_full_simp_tac 1);
 by (Asm_full_simp_tac 1);
 by (Blast_tac 1);
@@ -1467,19 +1467,19 @@
 	   sum_eq_0_conv]);
 
 Goal "take n (x#xs) = (if n = #0 then [] else x # take (n-#1) xs)";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
 by (ALLGOALS 
     (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1])));
 qed "take_Cons'";
 
 Goal "drop n (x#xs) = (if n = #0 then x#xs else drop (n-#1) xs)";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
 by (ALLGOALS
     (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1])));
 qed "drop_Cons'";
 
 Goal "(x#xs)!n = (if n = #0 then x else xs!(n-#1))";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
 by (ALLGOALS
     (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1])));
 qed "nth_Cons'";
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/MicroJava/BV/BVSpecTypeSafe.ML
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -68,7 +68,7 @@
 be widen.induct 1;
 by(Auto_tac);
 by(rename_tac "R" 1);
-by(exhaust_tac "R" 1);
+by(cases_tac "R" 1);
 by(Auto_tac);
 val lemma = result();
 
@@ -100,7 +100,7 @@
   ba 1;
  ba 1;
 by(rewtac wt_jvm_prog_def);
-by (exhaust_tac "ls_com" 1);
+by (cases_tac "ls_com" 1);
 by (ALLGOALS (fast_tac (claset() addIs [Load_correct,Store_correct,Bipush_correct,Aconst_null_correct])));
 qed "LS_correct";
 
@@ -119,7 +119,7 @@
 by (asm_full_simp_tac (simpset() addsimps [conf_def]) 1);
 by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [obj_ty_def]) 1);
-by (exhaust_tac "v" 1);
+by (cases_tac "v" 1);
 by (ALLGOALS (fast_tac  (claset() addIs [rtrancl_trans] addss (simpset() addsimps [widen.null]))));
 qed "Cast_conf2";
 
@@ -149,7 +149,7 @@
   ba 1;
  ba 1;
 by(rewtac wt_jvm_prog_def);
-by (exhaust_tac "ch_com" 1);
+by (cases_tac "ch_com" 1);
 by (ALLGOALS (fast_tac (claset() addIs [Checkcast_correct])));
 qed "CH_correct";
 
@@ -223,7 +223,7 @@
   ba 1;
  ba 1;
 by(rewtac wt_jvm_prog_def);
-by (exhaust_tac "mo_com" 1);
+by (cases_tac "mo_com" 1);
 by (ALLGOALS (fast_tac (claset() addIs [Getfield_correct,Putfield_correct])));
 qed "MO_correct";
 
@@ -263,7 +263,7 @@
   ba 1;
  ba 1;
 by(rewtac wt_jvm_prog_def);
-by (exhaust_tac "co_com" 1);
+by (cases_tac "co_com" 1);
 by (ALLGOALS (fast_tac (claset() addIs [New_correct])));
 qed "CO_correct";
 
@@ -282,7 +282,7 @@
 by(etac exE 1);
 by(asm_full_simp_tac (simpset() addsimps defs1) 1);
 by(Clarify_tac 1);
-by(exhaust_tac "X\\<noteq>NT" 1); 
+by(case_tac "X\\<noteq>NT" 1); 
  by (asm_full_simp_tac (simpset()addsimps[raise_xcpt_def]@defs1 
 	addsplits [option.split]) 1);
  by (Clarify_tac 1);
@@ -360,7 +360,7 @@
 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
   ba 1;
  ba 1;
-by (exhaust_tac "mi_com" 1);
+by (cases_tac "mi_com" 1);
 by (ALLGOALS (fast_tac (claset() addIs [Invoke_correct])));
 qed "MI_correct";
 
@@ -401,7 +401,7 @@
 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
   ba 1;
  ba 1;
-by (exhaust_tac "mr" 1);
+by (cases_tac "mr" 1);
 by (ALLGOALS (fast_tac (claset() addIs [Return_correct])));
 qed "MR_correct";
 
@@ -442,7 +442,7 @@
   ba 1;
  ba 1;
 by(rewtac wt_jvm_prog_def);
-by (exhaust_tac "br_com" 1);
+by (cases_tac "br_com" 1);
 by (ALLGOALS (fast_tac (claset() addIs [Goto_correct,Ifiacmpeq_correct])));
 qed "BR_correct";
 
@@ -521,7 +521,7 @@
   ba 1;
  ba 1;
 by(rewtac wt_jvm_prog_def);
-by (exhaust_tac "os_com" 1);
+by (cases_tac "os_com" 1);
 by (ALLGOALS (fast_tac (claset() addIs [Pop_correct,Dup_correct,Dup_x1_correct,Dup_x2_correct,Swap_correct])));
 qed "OS_correct";
 
@@ -539,15 +539,15 @@
 \ \\<Longrightarrow> exec (G,state) = Some state' \\<longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
 by(split_all_tac 1);
 by(rename_tac "xp hp frs" 1);
-by (exhaust_tac "xp" 1);
- by (exhaust_tac "frs" 1);
+by (cases_tac "xp" 1);
+ by (cases_tac "frs" 1);
   by (asm_full_simp_tac (simpset() addsimps exec.rules) 1);
  by(split_all_tac 1);
  by(hyp_subst_tac 1);
  by(forward_tac [correct_state_impl_Some_method] 1);
  by (force_tac (claset() addIs [LS_correct,CO_correct,MO_correct,CH_correct,MI_correct,MR_correct,OS_correct,
 	BR_correct], simpset() addsplits [split_if_asm,instr.split,instr.split_asm] addsimps exec.rules@[split_def]) 1);
-by (exhaust_tac "frs" 1);
+by (cases_tac "frs" 1);
  by (ALLGOALS(asm_full_simp_tac (simpset() addsimps exec.rules)));
 qed_spec_mp "BV_correct_1";
 
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/MicroJava/BV/Convert.ML
--- a/src/HOL/MicroJava/BV/Convert.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/MicroJava/BV/Convert.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -6,7 +6,7 @@
 
 
 Goalw[sup_ty_opt_def] "G \\<turnstile> t <=o t";
-by (exhaust_tac "t" 1);
+by (cases_tac "t" 1);
 by Auto_tac;
 qed "sup_ty_opt_refl";
 Addsimps [sup_ty_opt_refl];
@@ -66,7 +66,7 @@
 by (induct_tac "a" 1);
  by (Simp_tac 1);
 by (Clarsimp_tac 1);
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
  by (Asm_full_simp_tac 1);
 by (eres_inst_tac [("x","nat")] allE 1);
 by (smp_tac 1 1);
@@ -89,7 +89,7 @@
 by (induct_tac "a" 1);
  by (Clarsimp_tac 1);
 by (Clarify_tac 1);
-by (exhaust_tac "b" 1);
+by (cases_tac "b" 1);
  by (Clarsimp_tac 1);  
 by (Clarsimp_tac 1);
 qed_spec_mp "sup_loc_append";
@@ -112,7 +112,7 @@
 by (Clarsimp_tac 1);
 by Safe_tac;
  by (clarsimp_tac (claset(), simpset() addsimps [sup_loc_append, sup_loc_length]) 2);
-by (exhaust_tac "b" 1); 
+by (cases_tac "b" 1); 
  bd sup_loc_length 1;
  by (Clarsimp_tac 1);
 by (clarsimp_tac (claset(), simpset() addsimps [sup_loc_append, sup_loc_length]) 1);
@@ -129,7 +129,7 @@
 qed "sup_state_rev_fst";
 
 Goal "map x a = Y # YT \\<longrightarrow> map x (tl a) = YT \\<and> x (hd a) = Y \\<and> (\\<exists> y yt. a = y#yt)";
-by (exhaust_tac "a" 1);
+by (cases_tac "a" 1);
 by Auto_tac;
 qed_spec_mp "map_hd_tl";
 
@@ -159,15 +159,15 @@
 
 Goalw[sup_ty_opt_def] 
 "\\<lbrakk>G \\<turnstile> a <=o b; G \\<turnstile> b <=o c\\<rbrakk> \\<Longrightarrow> G \\<turnstile> a <=o c";
-by (exhaust_tac "c" 1);
+by (cases_tac "c" 1);
  by (Clarsimp_tac 1);
 by (Clarsimp_tac 1);
-by (exhaust_tac "a" 1);
+by (cases_tac "a" 1);
  by (Clarsimp_tac 1);
- by (exhaust_tac "b" 1);
+ by (cases_tac "b" 1);
   by (Clarsimp_tac 1);
  by (Clarsimp_tac 1);
-by (exhaust_tac "b" 1);
+by (cases_tac "b" 1);
  by (Clarsimp_tac 1);
 by (Clarsimp_tac 1);
 be widen_trans 1;
@@ -190,7 +190,7 @@
 by (induct_tac "a" 1);
  by (Clarsimp_tac 1);
 by (Clarsimp_tac 1);
-by (exhaust_tac "b=[]" 1);
+by (case_tac "b=[]" 1);
  by (Clarsimp_tac 1);
 by (Clarsimp_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
@@ -230,7 +230,7 @@
 qed "sup_state_trans";
 
 Goalw[sup_ty_opt_def] "G \\<turnstile> a <=o Some b \\<Longrightarrow> \\<exists> x. a = Some x";
-by (exhaust_tac "a" 1);
+by (cases_tac "a" 1);
  by Auto_tac;
 qed "sup_ty_opt_some";
 
@@ -240,7 +240,7 @@
 by (induct_tac "x" 1);
  by (Simp_tac 1);
 by (clarsimp_tac ((claset(), simpset()) addIffs [sup_loc_Cons2]) 1);
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
  by (clarsimp_tac (claset(), simpset() addsimps [list_all2_Cons1]) 1);
 by (clarsimp_tac (claset(), simpset() addsimps [list_all2_Cons1]) 1);
 qed_spec_mp "sup_loc_update";
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/MicroJava/BV/Correct.ML
--- a/src/HOL/MicroJava/BV/Correct.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/MicroJava/BV/Correct.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -40,7 +40,7 @@
 Goal
 "\\<lbrakk> wf_prog wt G \\<rbrakk> \
 \\\<Longrightarrow> approx_val G hp v (Some T) \\<longrightarrow> G\\<turnstile> T\\<preceq>T' \\<longrightarrow> approx_val G hp v (Some T')";
-by (exhaust_tac "T" 1);
+by (cases_tac "T" 1);
  by (Asm_simp_tac 1);
 by (fast_tac (claset() addIs [conf_widen] addss (simpset()addsimps[approx_val_def])) 1);
 qed_spec_mp "approx_val_imp_approx_val_assConvertible";
@@ -56,7 +56,7 @@
 Goal
 "\\<lbrakk> hp a = Some obj' ; G,hp\\<turnstile> v\\<Colon>\\<preceq>T ; obj_ty obj = obj_ty obj' \\<rbrakk> \
 \\\<Longrightarrow>G,(hp(a\\<mapsto>obj))\\<turnstile> v\\<Colon>\\<preceq>T";
-by (exhaust_tac "v" 1);
+by (cases_tac "v" 1);
 by (auto_tac (claset() , simpset() addsimps [obj_ty_def,conf_def] addsplits [option.split]));
 qed_spec_mp "approx_val_imp_approx_val_heap_update";
 
@@ -97,7 +97,7 @@
 
 Goalw [approx_loc_def,list_all2_def]
 "\\<forall> lvars. approx_loc G hp lvars lt \\<longrightarrow>  hp \\<le>| hp' \\<longrightarrow> approx_loc G hp' lvars lt";
-by (exhaust_tac "lt" 1);
+by (cases_tac "lt" 1);
  by (Asm_simp_tac 1);
 by (force_tac (claset() addIs [approx_val_imp_approx_val_sup_heap],
 	       simpset() addsimps [neq_Nil_conv]) 1);
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/MicroJava/BV/LBVComplete.ML
--- a/src/HOL/MicroJava/BV/LBVComplete.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/MicroJava/BV/LBVComplete.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -7,14 +7,14 @@
 by (induct_tac "a" 1);
  by (Clarsimp_tac 1);
 by (Clarsimp_tac 1);
-by (exhaust_tac "P n" 1);
+by (case_tac "P n" 1);
  by (Clarsimp_tac 1);
- by (exhaust_tac "na" 1);
+ by (cases_tac "na" 1);
   by (Clarsimp_tac 1);
  by (clarsimp_tac (claset(), simpset() addsimps [length_option_filter_n]) 1);
  by (Force_tac 1);
 by (Clarsimp_tac 1);
-by (exhaust_tac "na" 1);
+by (cases_tac "na" 1);
  by (Clarsimp_tac 1);
 by (force_tac (claset(), simpset() addsimps [length_option_filter_n]) 1);
 qed_spec_mp "is_approx_option_filter_n";
@@ -28,7 +28,7 @@
 by (induct_tac "l" 1);
  by (Simp_tac 1);
 by (Clarify_tac 1);
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
  by (Clarsimp_tac 1);
 by (Clarsimp_tac 1);
 qed_spec_mp "option_filter_n_Some";
@@ -90,7 +90,7 @@
 by (induct_tac "x" 1);
  by (Simp_tac 1);
 by (Clarsimp_tac 1);
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
  by (Clarsimp_tac 1);
 by (Clarsimp_tac 1);
 by (smp_tac 1 1);
@@ -114,13 +114,13 @@
 
 
 Goal "G \\<turnstile> b \\<preceq> NT \\<Longrightarrow> b = NT";
-by (exhaust_tac "b" 1);
- by (exhaust_tac "ref_ty" 2);
+by (cases_tac "b" 1);
+ by (cases_tac "ref_ty" 2);
 by Auto_tac;
 qed "widen_NT";
 
 Goal "G \\<turnstile> b \\<preceq> Class C \\<Longrightarrow> \\<exists>r. b = RefT r";
-by (exhaust_tac "b" 1);
+by (cases_tac "b" 1);
 by Auto_tac;
 qed "widen_Class";
 
@@ -129,7 +129,7 @@
 by (induct_tac "a" 1);
  by (Clarsimp_tac 1);
 by (Clarsimp_tac 1);
-by (exhaust_tac "b" 1);
+by (cases_tac "b" 1);
  by (Clarsimp_tac 1);
 by (Clarsimp_tac 1);
 qed_spec_mp "all_widen_is_sup_loc";
@@ -139,7 +139,7 @@
 \      G \\<turnstile> (x, y) <=s s1; wtl_inst i G rT s1 s1' cert mpc pc\\<rbrakk> \
 \       \\<Longrightarrow> \\<exists>s2'. wtl_inst i G rT (x, y) s2' cert mpc pc \\<and> \
 \                ((G \\<turnstile> s2' <=s s1') \\<or> (\\<exists> s. cert ! (Suc pc) = Some s \\<and> (G \\<turnstile> s2' <=s s)))"; 
-by (exhaust_tac "meth_inv" 1); 
+by (cases_tac "meth_inv" 1); 
 by (Clarsimp_tac 1);
 by (cut_inst_tac [("x","x"),("n","length apTs")] rev_append_cons 1);
  by (asm_full_simp_tac (simpset() addsimps [sup_state_length_fst]) 1);
@@ -150,7 +150,7 @@
 back();
 back();
 by (clarsimp_tac (claset(), simpset() addsimps [sup_state_rev_fst,sup_state_Cons1]) 1);
-by (exhaust_tac "X = NT" 1);
+by (case_tac "X = NT" 1);
  by (Clarsimp_tac 1);
  by (res_inst_tac [("x","a")] exI 1);
  by (res_inst_tac [("x","b")] exI 1);
@@ -161,7 +161,7 @@
 by (strip_tac1 1);
 by (forward_tac [widen_Class] 1);
 by (Clarsimp_tac 1);
-by (exhaust_tac "r" 1);
+by (cases_tac "r" 1);
  by (Clarsimp_tac 1);
  by (res_inst_tac [("x","a")] exI 1);
  by (res_inst_tac [("x","b")] exI 1);
@@ -198,7 +198,7 @@
 by (induct_tac "b" 1);
  by (Simp_tac 1);
 by (clarsimp_tac (claset(), simpset() addsimps [list_all2_Cons1]) 1);
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
  by (asm_full_simp_tac (simpset() addsimps [sup_ty_opt_some]) 1);
 by (smp_tac 1 1);
 by (Asm_full_simp_tac 1);
@@ -224,7 +224,7 @@
 
 Goal "(G \\<turnstile> xb \\<preceq> PrimT p) = (xb = PrimT p)";
 by Safe_tac;
-by (exhaust_tac "xb" 1);
+by (cases_tac "xb" 1);
 by Auto_tac;
 bd widen_RefT 1;
 by Auto_tac;
@@ -237,8 +237,8 @@
 \      (G \\<turnstile> s2' <=s s1' \\<or> (\\<exists>s. cert!(Suc pc) = Some s \\<and> G \\<turnstile> s2' <=s s))"; 
 by (cut_inst_tac [("z","s2")] surj_pair 1); 
 by (Clarify_tac 1); 
-by (exhaust_tac "ins!pc" 1); 
-       by (exhaust_tac "load_and_store" 1); 
+by (cases_tac "ins!pc" 1); 
+       by (cases_tac "load_and_store" 1); 
           by (Clarsimp_tac 1); 
           by (datac mono_load 2 1); 
           by (clarsimp_tac (claset(), simpset() addsimps [sup_state_length_snd]) 1);
@@ -247,9 +247,9 @@
          by (Clarsimp_tac 1);
         by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons1]) 1); 
        by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons1]) 1); 
-      by (exhaust_tac "create_object" 1); 
+      by (cases_tac "create_object" 1); 
       by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons1]) 1); 
-     by (exhaust_tac "manipulate_object" 1); 
+     by (cases_tac "manipulate_object" 1); 
       by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
       be widen_trans 1; 
       ba 1; 
@@ -259,7 +259,7 @@
       ba 1; 
      be widen_trans 1; 
      ba 1; 
-    by (exhaust_tac "check_object" 1); 
+    by (cases_tac "check_object" 1); 
     by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
     be widen_RefT2 1; 
     br method_inv_pseudo_mono 1;
@@ -270,7 +270,7 @@
       ba 1;
      ba 1;
     ba 1;   
-   by (exhaust_tac "meth_ret" 1);
+   by (cases_tac "meth_ret" 1);
    by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
    br conjI 1;
     be widen_trans 1;
@@ -278,13 +278,13 @@
    by (cut_inst_tac [("z","s1'")] surj_pair 1);
    by (strip_tac1 1);
    by (Clarsimp_tac 1);
-  by (exhaust_tac "op_stack" 1);
+  by (cases_tac "op_stack" 1);
      by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
     by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
    by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
   by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
  by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
-by (exhaust_tac "branch" 1);
+by (cases_tac "branch" 1);
  by (Clarsimp_tac 1);
  bd sup_state_trans 1;
   ba 1;
@@ -298,10 +298,10 @@
   ba 2;
  ba 2;
 by (Clarsimp_tac 1);
-by (exhaust_tac "xa" 1);
+by (cases_tac "xa" 1);
  by (clarsimp_tac (claset(), simpset() addsimps [PrimT_PrimT]) 1);
 by (Clarsimp_tac 1);
-by (exhaust_tac "xb" 1);
+by (cases_tac "xb" 1);
 by Auto_tac;
 bd widen_RefT 1;
 by Auto_tac;
@@ -310,15 +310,15 @@
 
 Goal "\\<lbrakk>wtl_inst i G rT s1 s1' cert (Suc pc) pc; G \\<turnstile> s2 <=s s1\\<rbrakk> \\<Longrightarrow> \
 \ \\<exists>s2'. wtl_inst i G rT s2 s2' cert (Suc pc) pc \\<and> (G \\<turnstile> s2' <=s s1')";
-by (exhaust_tac "i" 1);
-by (exhaust_tac "branch" 8);
-by (exhaust_tac "op_stack" 7);
-by (exhaust_tac "meth_ret" 6);
-by (exhaust_tac "meth_inv" 5);
-by (exhaust_tac "check_object" 4);
-by (exhaust_tac "manipulate_object" 3);
-by (exhaust_tac "create_object" 2);
-by (exhaust_tac "load_and_store" 1);
+by (cases_tac "i" 1);
+by (cases_tac "branch" 8);
+by (cases_tac "op_stack" 7);
+by (cases_tac "meth_ret" 6);
+by (cases_tac "meth_inv" 5);
+by (cases_tac "check_object" 4);
+by (cases_tac "manipulate_object" 3);
+by (cases_tac "create_object" 2);
+by (cases_tac "load_and_store" 1);
 by (TRYALL Asm_full_simp_tac);
  by (pair_tac "s1'" 1);
  by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1);
@@ -335,7 +335,7 @@
 Goalw [wtl_inst_option_def] 
 "\\<lbrakk>wtl_inst_option i G rT s1 s1' cert mpc pc; Suc pc = mpc; G \\<turnstile> s2 <=s s1\\<rbrakk> \\<Longrightarrow> \
 \ \\<exists>s2'. wtl_inst_option i G rT s2 s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')";
-by (exhaust_tac "cert!pc" 1);
+by (cases_tac "cert!pc" 1);
  by (Clarsimp_tac 1);
  bd wtl_inst_last_mono 1;
   ba 1;
@@ -355,18 +355,18 @@
 \     \\<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";  
 by (cut_inst_tac [("z","phi!pc")] surj_pair 1);
 by (strip_tac1 1);
-by (exhaust_tac "ins!pc" 1);
-by (exhaust_tac "op_stack" 7);
-by (exhaust_tac "check_object" 4);
-by (exhaust_tac "manipulate_object" 3);
-by (exhaust_tac "create_object" 2);
-by (exhaust_tac "load_and_store" 1);
+by (cases_tac "ins!pc" 1);
+by (cases_tac "op_stack" 7);
+by (cases_tac "check_object" 4);
+by (cases_tac "manipulate_object" 3);
+by (cases_tac "create_object" 2);
+by (cases_tac "load_and_store" 1);
                by (TRYALL (Asm_full_simp_tac THEN_MAYBE' Force_tac));
-  by (exhaust_tac "meth_inv" 1);
+  by (cases_tac "meth_inv" 1);
   by (cut_inst_tac [("z","phi!(Suc pc)")] surj_pair 1);
   by (strip_tac1 1);
   by (Clarsimp_tac 1);
-  by (exhaust_tac "X = NT" 1);
+  by (case_tac "X = NT" 1);
    by (clarsimp_tac (claset(),simpset() addsimps [fits_def, contains_dead_def]) 1);
    by (smp_tac 1 1);
    by (Clarsimp_tac 1);
@@ -378,12 +378,12 @@
   by (Asm_full_simp_tac 1);
   by (res_inst_tac [("x","apTs")] exI 1);
   by (clarsimp_tac (claset(),simpset() addsimps [fits_def, contains_dead_def]) 1);
- by (exhaust_tac "meth_ret" 1);
+ by (cases_tac "meth_ret" 1);
  by (asm_full_simp_tac (simpset() addsimps [fits_def, contains_dead_def]) 1);
  by (cut_inst_tac [("z","phi!Suc pc")] surj_pair 1);
  by (strip_tac1 1);
  by (Clarsimp_tac 1);
-by (exhaust_tac "branch" 1);
+by (cases_tac "branch" 1);
  by (asm_full_simp_tac (simpset() addsimps [fits_def, contains_dead_def, contains_targets_def]) 1);
  by (cut_inst_tac [("z","phi!Suc pc")] surj_pair 1);
  by (Force_tac 1);
@@ -395,7 +395,7 @@
      "\\<lbrakk>fits ins cert phi; pc < length ins; wt_instr (ins!pc) G rT phi max_pc pc; \
 \      max_pc = length ins\\<rbrakk> \\<Longrightarrow> \ 
 \     \\<exists> s. wtl_inst_option (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";
-by (exhaust_tac "cert!pc" 1);
+by (cases_tac "cert!pc" 1);
  by (Clarsimp_tac 1);
  bd wt_instr_imp_wtl_inst 1;
     ba 1;
@@ -417,14 +417,14 @@
 \     ins \\<noteq> []; G \\<turnstile> s <=s s0; \ 
 \     s \\<noteq> s0 \\<longrightarrow> cert ! pc = Some s0\\<rbrakk> \\<Longrightarrow> \ 
 \     wtl_inst_list ins G rT s s' cert max_pc pc";  
-by (exhaust_tac "ins" 1); 
+by (cases_tac "ins" 1); 
  by (Clarify_tac 1);
 by (Clarify_tac 1);
 by (Asm_full_simp_tac 1);
 by (Clarify_tac 1);
-by (exhaust_tac "list = []" 1);
+by (case_tac "list = []" 1);
  by (Asm_full_simp_tac 1);
- by (exhaust_tac "s = s0" 1);
+ by (case_tac "s = s0" 1);
   by (Force_tac 1);
  by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
 by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
@@ -434,7 +434,7 @@
 Goal "\\<lbrakk>wtl_inst_list ins G rT s0 s' cert max_pc pc; \ 
 \     ins \\<noteq> []; G \\<turnstile> s <=s s0; cert ! pc = Some s0\\<rbrakk> \\<Longrightarrow> \ 
 \     wtl_inst_list ins G rT s s' cert max_pc pc"; 
-by (exhaust_tac "ins" 1); 
+by (cases_tac "ins" 1); 
  by (Clarify_tac 1);
 by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
 qed "wtl_inst_list_cert";
@@ -446,7 +446,7 @@
 \ G \\<turnstile> s2 <=s s1; i = ins!pc\\<rbrakk> \\<Longrightarrow> \
 \ \\<exists> s2'. wtl_inst_option (ins!pc) G rT s2 s2' cert mpc pc \\<and> \
 \        (G \\<turnstile> s2' <=s s1' \\<or> (\\<exists>s. cert!(Suc pc) = Some s \\<and> G \\<turnstile> s2' <=s s))";
-by (exhaust_tac "cert!pc" 1);
+by (cases_tac "cert!pc" 1);
  by (Asm_full_simp_tac 1);
  by (datac wtl_inst_pseudo_mono 4 1);
   by (Clarsimp_tac 1);
@@ -495,7 +495,7 @@
  by (Simp_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [nth_append]) 1);
 by (Clarify_tac 1);
-by (exhaust_tac "list = []" 1);
+by (case_tac "list = []" 1);
  by (Clarsimp_tac 1);
  bd wtl_option_last_mono 1;
    br refl 1;
@@ -512,7 +512,7 @@
   ba 1;
  by (simp_tac (simpset() addsimps [append_cons_length_nth]) 1);
 by (clarsimp_tac (claset(), simpset() addsimps [append_cons_length_nth]) 1);
-by (exhaust_tac "cert ! Suc (length l)" 1);
+by (cases_tac "cert ! Suc (length l)" 1);
  by (Clarsimp_tac 1);
  by (dres_inst_tac [("a","(ac,bb)")] sup_state_trans 1);
   ba 1;
@@ -529,7 +529,7 @@
 by (clarsimp_tac (claset(), simpset() addsimps [fits_def, is_approx_def]) 1);
 by (eres_inst_tac [("x","Suc (length l)")] allE 1);
 be impE 1;
- by (exhaust_tac "length list" 1);
+ by (cases_tac "length list" 1);
   by (Clarsimp_tac 1);
  by (Clarsimp_tac 1);
 by (Clarsimp_tac 1);
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/MicroJava/BV/LBVCorrect.ML
--- a/src/HOL/MicroJava/BV/LBVCorrect.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/MicroJava/BV/LBVCorrect.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -25,11 +25,11 @@
 by (eres_inst_tac [("x","Suc pc")] allE 1);
 by (Asm_full_simp_tac 1);
 by (Clarify_tac 1);
-by (exhaust_tac "cert ! pc" 1);
+by (cases_tac "cert ! pc" 1);
  by (res_inst_tac [("x","phi[pc:=(aa, b)]")] exI 1);
  by (asm_full_simp_tac (simpset() addsimps [fits_partial_def]) 1);
  by (Clarify_tac 1);
- by (exhaust_tac "ac" 1);
+ by (cases_tac "ac" 1);
   by (Asm_full_simp_tac 1);
  by (Asm_full_simp_tac 1);
  by (Clarify_tac 1);
@@ -46,7 +46,7 @@
 by (res_inst_tac [("x","phi[pc:=ac]")] exI 1);
 by (asm_full_simp_tac (simpset() addsimps [fits_partial_def]) 1);
 by (Clarify_tac 1);
-by (exhaust_tac "ad" 1);
+by (cases_tac "ad" 1);
  by (Asm_full_simp_tac 1);
 by (Asm_full_simp_tac 1);
 by (Clarify_tac 1);
@@ -94,13 +94,13 @@
 by (forward_tac [wtl_append] 1);
   ba 1;
  ba 1;
-by (exhaust_tac "b=[]" 1);
+by (case_tac "b=[]" 1);
  by (Asm_full_simp_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
 by (Clarify_tac 1);
 by (Asm_full_simp_tac 1);
 by (Clarify_tac 1);
-by (exhaust_tac "cert!(Suc (length a))" 1);
+by (cases_tac "cert!(Suc (length a))" 1);
  by (asm_full_simp_tac (simpset() addsimps [fits_def, fits_partial_def]) 1);
  by (eres_inst_tac [("x","a@[i]")] allE 1);
  by (eres_inst_tac [("x","ys")] allE 1);
@@ -161,46 +161,46 @@
 by (TRYALL atac);
 by (forward_tac [fits_lemma1] 1);
  ba 1;
-by (exhaust_tac "cert!(length i1)" 1);
+by (cases_tac "cert!(length i1)" 1);
  by (forward_tac [fits_lemma2] 1);
      by (TRYALL atac);
- by (exhaust_tac "i" 1);
-        by (exhaust_tac "check_object" 4);
-        by (exhaust_tac "manipulate_object" 3);
-         by (exhaust_tac "create_object" 2);
-         by (exhaust_tac "load_and_store" 1);
+ by (cases_tac "i" 1);
+        by (cases_tac "check_object" 4);
+        by (cases_tac "manipulate_object" 3);
+         by (cases_tac "create_object" 2);
+         by (cases_tac "load_and_store" 1);
             by (GOALS (force_tac (claset(), 
                 simpset() addsimps [wt_instr_def,wtl_inst_option_def])) 1 8);
-    by (exhaust_tac "meth_inv" 1);
+    by (cases_tac "meth_inv" 1);
     by (thin_tac "\\<forall>pc t.\
 \                 pc < length (i1 @ i # i2) \\<longrightarrow> \
 \                 cert ! pc = Some t \\<longrightarrow> phi ! pc = t" 1);
     by (pair_tac "s1" 1);
     by (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 1);    
     by (Force_tac 1);
-   by (exhaust_tac "meth_ret" 1);
+   by (cases_tac "meth_ret" 1);
    by (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 1);
-  by (exhaust_tac "branch" 2);
-   by (exhaust_tac "op_stack" 1);
+  by (cases_tac "branch" 2);
+   by (cases_tac "op_stack" 1);
        by (GOALS (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 
                   THEN_MAYBE' Force_tac) 1 7);
 by (forw_inst_tac [("x","length i1")] spec 1);
 by (eres_inst_tac [("x","a")] allE 1);
-by (exhaust_tac "i" 1);
-       by (exhaust_tac "check_object" 4);
-       by (exhaust_tac "manipulate_object" 3);
-        by (exhaust_tac "create_object" 2);
-        by (exhaust_tac "load_and_store" 1);
+by (cases_tac "i" 1);
+       by (cases_tac "check_object" 4);
+       by (cases_tac "manipulate_object" 3);
+        by (cases_tac "create_object" 2);
+        by (cases_tac "load_and_store" 1);
            by (GOALS (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 
                       THEN' Force_tac) 1 8);
-   by (exhaust_tac "meth_inv" 1);
+   by (cases_tac "meth_inv" 1);
    by (thin_tac "\\<forall>pc t.\
 \                pc < length (i1 @ i # i2) \\<longrightarrow> \
 \                cert ! pc = Some t \\<longrightarrow> phi ! pc = t" 1);
    by (force_tac (claset(), simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 1);
-  by (exhaust_tac "branch" 3);
-   by (exhaust_tac "op_stack" 2);
-       by (exhaust_tac "meth_ret" 1);
+  by (cases_tac "branch" 3);
+   by (cases_tac "op_stack" 2);
+       by (cases_tac "meth_ret" 1);
        by (GOALS (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 
                   THEN_MAYBE' Force_tac) 1 8);
 qed "wtl_lemma";
@@ -242,7 +242,7 @@
 by (Asm_full_simp_tac 1);
 be impE 1;
 by (Force_tac 1);
-by (exhaust_tac "cert ! 0" 1);
+by (cases_tac "cert ! 0" 1);
 by (auto_tac (claset(), simpset() addsimps [wtl_inst_option_def]));
 qed "fits_first";
 
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/MicroJava/BV/LBVSpec.ML
--- a/src/HOL/MicroJava/BV/LBVSpec.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/MicroJava/BV/LBVSpec.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -11,15 +11,15 @@
 
 Goal "\\<lbrakk>wtl_inst i G rT s0 s1 cert max_pc pc; \
 \      wtl_inst i G rT s0 s1' cert max_pc pc\\<rbrakk> \\<Longrightarrow> s1 = s1'";
-by (exhaust_tac "i" 1);
-by (exhaust_tac "branch" 8);
-by (exhaust_tac "op_stack" 7);
-by (exhaust_tac "meth_ret" 6);
-by (exhaust_tac "meth_inv" 5);
-by (exhaust_tac "check_object" 4);
-by (exhaust_tac "manipulate_object" 3);
-by (exhaust_tac "create_object" 2);
-by (exhaust_tac "load_and_store" 1);
+by (cases_tac "i" 1);
+by (cases_tac "branch" 8);
+by (cases_tac "op_stack" 7);
+by (cases_tac "meth_ret" 6);
+by (cases_tac "meth_inv" 5);
+by (cases_tac "check_object" 4);
+by (cases_tac "manipulate_object" 3);
+by (cases_tac "create_object" 2);
+by (cases_tac "load_and_store" 1);
 by Auto_tac;
 by (ALLGOALS (dtac rev_eq));
 by (TRYALL atac);
@@ -29,7 +29,7 @@
 
 Goal "\\<lbrakk>wtl_inst_option i G rT s0 s1 cert max_pc pc; \
 \      wtl_inst_option i G rT s0 s1' cert max_pc pc\\<rbrakk> \\<Longrightarrow> s1 = s1'";
-by (exhaust_tac "cert!pc" 1);
+by (cases_tac "cert!pc" 1);
 by (auto_tac (claset(), simpset() addsimps [wtl_inst_unique, wtl_inst_option_def]));
 qed "wtl_inst_option_unique";
 
@@ -49,12 +49,12 @@
 \                  wtl_inst_list b G rT s1 s' cert mpc (pc+length a))";
 by(induct_tac "is" 1);
  by Auto_tac;
-by (exhaust_tac "pc'" 1);
+by (cases_tac "pc'" 1);
  by (dres_inst_tac [("x","pc'")] spec 1);
  by (smp_tac 3 1);
  by (res_inst_tac [("x","[]")] exI 1);
  by (Asm_full_simp_tac 1);
- by (exhaust_tac "cert!pc" 1);
+ by (cases_tac "cert!pc" 1);
   by (Force_tac 1);
  by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
 by (dres_inst_tac [("x","nat")] spec 1);
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/MicroJava/J/JBasis.ML
--- a/src/HOL/MicroJava/J/JBasis.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/MicroJava/J/JBasis.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -83,7 +83,7 @@
 	eresolve_tac prems 1]);
 
 fun option_case_tac2 s i = EVERY [
-	 exhaust_tac s i,
+	 cases_tac s i,
 	 rotate_tac ~1 (i+1), asm_full_simp_tac HOL_basic_ss (i+1), 
 	 rotate_tac ~1  i   , asm_full_simp_tac HOL_basic_ss i];
 
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/MicroJava/J/JTypeSafe.ML
--- a/src/HOL/MicroJava/J/JTypeSafe.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -284,7 +284,7 @@
 (* Level 45 *)
 
 (* 1 Call *)
-by( exhaust_tac "x" 1);
+by( cases_tac "x" 1);
 by(  Clarsimp_tac 2);
 by(  dtac exec_xcpt 2);
 by(  Asm_full_simp_tac 2);
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/MicroJava/J/Type.ML
--- a/src/HOL/MicroJava/J/Type.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/MicroJava/J/Type.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -5,6 +5,6 @@
 *)
 
 Goal "(\\<forall>pt. T \\<noteq> PrimT pt) = (\\<exists>t. T = RefT t)";
-by(exhaust_tac "T" 1);
+by(cases_tac "T" 1);
 by Auto_tac;
 qed "non_PrimT";
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Nat.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -22,23 +22,23 @@
 val [nat_case_0, nat_case_Suc] = nat.cases;
 
 Goal "n ~= 0 ==> EX m. n = Suc m";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
 by (REPEAT (Blast_tac 1));
 qed "not0_implies_Suc";
 
 Goal "m<n ==> n ~= 0";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "gr_implies_not0";
 
 Goal "(n ~= 0) = (0 < n)";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
 by Auto_tac;
 qed "neq0_conv";
 AddIffs [neq0_conv];
 
 Goal "(0 ~= n) = (0 < n)";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
 by Auto_tac;
 qed "zero_neq_conv";
 AddIffs [zero_neq_conv];
@@ -64,7 +64,7 @@
 
 (*Useful in certain inductive arguments*)
 Goal "(m < Suc n) = (m=0 | (EX j. m = Suc j & j < n))";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
 by Auto_tac;
 qed "less_Suc_eq_0_disj";
 
@@ -74,11 +74,11 @@
 by (fold_goals_tac [Least_nat_def]);
 by (safe_tac (claset() addSEs [LeastI]));
 by (rename_tac "j" 1);
-by (exhaust_tac "j" 1);
+by (cases_tac "j" 1);
 by (Blast_tac 1);
 by (blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1);
 by (rename_tac "k n" 1);
-by (exhaust_tac "k" 1);
+by (cases_tac "k" 1);
 by (Blast_tac 1);
 by (hyp_subst_tac 1);
 by (rewtac Least_nat_def);
@@ -90,8 +90,8 @@
 
 val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
 by (rtac less_induct 1);
-by (exhaust_tac "n" 1);
-by (exhaust_tac "nat" 2);
+by (cases_tac "n" 1);
+by (cases_tac "nat" 2);
 by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans])));
 qed "nat_induct2";
 
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/Option.ML
--- a/src/HOL/Option.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Option.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -82,13 +82,13 @@
 
 
 Goal "x : o2s xo = (xo = Some x)";
-by (exhaust_tac "xo" 1);
+by (cases_tac "xo" 1);
 by Auto_tac;
 qed "elem_o2s";
 AddIffs [elem_o2s];
 
 Goal "(o2s xo = {}) = (xo = None)";
-by (exhaust_tac "xo" 1);
+by (cases_tac "xo" 1);
 by Auto_tac;
 qed "o2s_empty_eq";
 
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/Power.ML
--- a/src/HOL/Power.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Power.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -48,7 +48,7 @@
 (*** Binomial Coefficients, following Andy Gordon and Florian Kammueller ***)
 
 Goal "(n choose 0) = 1";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "binomial_n_0";
 
@@ -99,7 +99,7 @@
 by (induct_tac "n" 1);
 by (simp_tac (simpset() addsimps [binomial_0]) 1);
 by (Clarify_tac 1);
-by (exhaust_tac "k" 1);
+by (cases_tac "k" 1);
 by (auto_tac (claset(),
 	      simpset() addsimps [add_mult_distrib, add_mult_distrib2,
 				  le_Suc_eq, binomial_eq_0]));
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/Real/RealPow.ML
--- a/src/HOL/Real/RealPow.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Real/RealPow.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -234,7 +234,7 @@
 qed_spec_mp "realpow_Suc_le";
 
 Goal "0r <= 0r ^ n";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
 by (Auto_tac);
 qed "realpow_zero_le";
 Addsimps [realpow_zero_le];
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/RelPow.ML
--- a/src/HOL/RelPow.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/RelPow.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -43,7 +43,7 @@
 \       !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P  \
 \    |] ==> P";
 by (cut_facts_tac [p1] 1);
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
 by (asm_full_simp_tac (simpset() addsimps [p2]) 1);
 by (Asm_full_simp_tac 1);
 by (etac compEpair 1);
@@ -70,7 +70,7 @@
 \       !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P  \
 \    |] ==> P";
 by (cut_facts_tac [p1] 1);
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
 by (asm_full_simp_tac (simpset() addsimps [p2]) 1);
 by (Asm_full_simp_tac 1);
 by (etac compEpair 1);
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/TLA/Inc/Inc.ML
--- a/src/HOL/TLA/Inc/Inc.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/TLA/Inc/Inc.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -165,7 +165,7 @@
   (fn _ => [auto_tac (Inc_css addsimps2 Init_defs
                               addSIs2 [(temp_use N2_leadsto_a) 
                                        RSN(2, (temp_use leadsto_init))]),
-	    exhaust_tac "pc2 (st1 sigma)" 1,
+	    cases_tac "pc2 (st1 sigma)" 1,
 	    Auto_tac
 	   ]);
 
@@ -212,7 +212,7 @@
   (fn _ => [auto_tac (Inc_css addsimps2 Init_defs
                               addSIs2 [(temp_use N1_leadsto_b) 
                                        RSN(2, temp_use leadsto_init)]),
-	    exhaust_tac "pc1 (st1 sigma)" 1,
+	    cases_tac "pc1 (st1 sigma)" 1,
 	    Auto_tac
 	   ]);
 
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/TLA/Memory/Memory.ML
--- a/src/HOL/TLA/Memory/Memory.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/TLA/Memory/Memory.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -123,7 +123,7 @@
 \        --> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))" (K [
 	     auto_tac (mem_css addsimps2 [enabled_disj]
 		                  addSIs2 [RWRNext_enabled]),
-             exhaust_tac "arg(ch w p)" 1,
+             cases_tac "arg(ch w p)" 1,
  	      action_simp_tac (simpset()addsimps[Read_def,enabled_ex])
 	                      [ReadInner_enabled,exI] [] 1,
               force_tac (mem_css addDs2 [base_pair]) 1,
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/UNITY/GenPrefix.ML
--- a/src/HOL/UNITY/GenPrefix.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/UNITY/GenPrefix.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -129,7 +129,7 @@
 
 Goal "((xs, y#ys) : genPrefix r) = \
 \     (xs=[] | (EX z zs. xs=z#zs & (z,y) : r & (zs,ys) : genPrefix r))";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
 by Auto_tac;
 qed "genPrefix_Cons";
 
@@ -183,7 +183,7 @@
 \               --> (xs, ys) : genPrefix r --> (xs ! i, ys ! i) : r";
 by (induct_tac "xs" 1);
 by Auto_tac;
-by (exhaust_tac "i" 1);
+by (cases_tac "i" 1);
 by Auto_tac;
 qed_spec_mp "genPrefix_imp_nth";
 
@@ -194,7 +194,7 @@
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq_0_disj, 
 						all_conj_distrib])));
 by (Clarify_tac 1);
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
 by (ALLGOALS Force_tac);
 qed_spec_mp "nth_imp_genPrefix";
 
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/UNITY/Lift_prog.ML
--- a/src/HOL/UNITY/Lift_prog.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/UNITY/Lift_prog.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -16,7 +16,7 @@
 Goal "(insert_map i x (delete_map i g)) = g(i:=x)";
 by (rtac ext 1);
 by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
-by (exhaust_tac "d" 1);
+by (cases_tac "d" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "insert_map_delete_map_eq";
 
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/UNITY/TimerArray.ML
--- a/src/HOL/UNITY/TimerArray.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/UNITY/TimerArray.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -15,7 +15,7 @@
 Goal "Timer : UNIV leadsTo {s. count s = 0}";
 by (res_inst_tac [("f", "count")] lessThan_induct 1);
 by (Simp_tac 1);
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
 by (force_tac (claset() addSIs [subset_imp_leadsTo], simpset()) 1);
 by (ensures_tac "decr" 1);
 qed "Timer_leadsTo_zero";
@@ -36,7 +36,7 @@
 by (constrains_tac 2);
 (*Progress property for the array of Timers*)
 by (res_inst_tac [("f", "sub i o fst")] lessThan_induct 1);
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
 (*Annoying need to massage the conditions to have the form (... Times UNIV)*)
 by (auto_tac (claset() addIs [subset_imp_leadsTo], 
 	      simpset() addsimps [insert_absorb, lessThan_Suc RS sym,
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/UNITY/Token.ML
--- a/src/HOL/UNITY/Token.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/UNITY/Token.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -16,7 +16,7 @@
 
 Goalw Token_defs "(s ~: E i) = (s : H i | s : T i)";
 by (Simp_tac 1);
-by (exhaust_tac "proc s i" 1);
+by (cases_tac "proc s i" 1);
 by Auto_tac;
 qed "not_E_eq";
 
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/ex/BinEx.ML
--- a/src/HOL/ex/BinEx.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/ex/BinEx.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -323,13 +323,13 @@
 
 Goal "w: normal ==> bin_succ w : normal";
 by (etac normal.induct 1);
-by (exhaust_tac "w" 4);
+by (cases_tac "w" 4);
 by (auto_tac (claset(), simpset() addsimps [NCons_True, bin_succ_BIT]));
 qed "bin_succ_normal";
 
 Goal "w: normal ==> bin_pred w : normal";
 by (etac normal.induct 1);
-by (exhaust_tac "w" 3);
+by (cases_tac "w" 3);
 by (auto_tac (claset(), simpset() addsimps [NCons_False, bin_pred_BIT]));
 qed "bin_pred_normal";
 
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/ex/Factorization.ML
--- a/src/HOL/ex/Factorization.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/ex/Factorization.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -10,12 +10,12 @@
 (* --- Arithmetic --- *)
 
 Goal "[| m ~= m*k; m ~= 1 |] ==> 1<m";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
 by Auto_tac;
 qed "one_less_m";
 
 Goal "[| m ~= m*k; 1<m*k |] ==> 1<k";
-by (exhaust_tac "k" 1);
+by (cases_tac "k" 1);
 by Auto_tac;
 qed "one_less_k";
 
@@ -24,7 +24,7 @@
 qed "mult_left_cancel";
 
 Goal "[| 0<m; m*n = m |] ==> n=1";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
 by Auto_tac;
 qed "mn_eq_m_one";
 
@@ -55,7 +55,7 @@
 
 Goalw [prime_def,dvd_def] "p:prime ==> ~(p dvd 1)";
 by Auto_tac;
-by (exhaust_tac "k" 1);
+by (cases_tac "k" 1);
 by Auto_tac;
 qed "prime_nd_one";
 
@@ -78,7 +78,7 @@
 qed "primes_eq";
 
 Goalw [primel_def,prime_def] "[| primel xs; prod xs = 1 |] ==> xs = []";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "primel_one_empty";
 
@@ -105,7 +105,7 @@
 
 Goal "nondec xs --> nondec (oinsert x xs)";
 by (induct_tac "xs" 1);
-by (exhaust_tac "list" 2);
+by (cases_tac "list" 2);
 by (ALLGOALS (Asm_full_simp_tac));
 qed_spec_mp "nondec_oinsert";
 
@@ -123,9 +123,9 @@
 by (induct_tac "xs" 1);
 by Safe_tac;
 by (ALLGOALS Asm_full_simp_tac);
-by (exhaust_tac "list" 1);
+by (cases_tac "list" 1);
 by (ALLGOALS Asm_full_simp_tac);
-by (exhaust_tac "list" 1);
+by (cases_tac "list" 1);
 by (Asm_full_simp_tac 1);
 by (res_inst_tac [("y","aa"),("ys","lista")] x_less_y_oinsert 1); 
 by (ALLGOALS Asm_full_simp_tac);
@@ -269,7 +269,7 @@
 \     --> xs <~~> ys)";
 by (res_inst_tac [("n","n")] less_induct 1);
 by Safe_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
 by (force_tac (claset() addIs [primel_one_empty], simpset()) 1);
 by (rtac (perm_primel_ex RS exE) 1);
 by (ALLGOALS Asm_full_simp_tac);
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/ex/Primrec.ML
--- a/src/HOL/ex/Primrec.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/ex/Primrec.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -185,7 +185,7 @@
 by (induct_tac "l" 1);
 by (ALLGOALS Asm_simp_tac);
 by (rtac allI 1);
-by (exhaust_tac "i" 1);
+by (cases_tac "i" 1);
 by (asm_simp_tac (simpset() addsimps [le_add1, le_imp_less_Suc]) 1);
 by (Asm_simp_tac 1);
 by (blast_tac (claset() addIs [less_le_trans] 
@@ -223,7 +223,7 @@
  "[| ALL l. f l + list_add l < ack(kf, list_add l); \
 \    ALL l. g l + list_add l < ack(kg, list_add l)  \
 \ |] ==> PREC f g l + list_add l < ack(Suc(kf+kg), list_add l)";
-by (exhaust_tac "l" 1);
+by (cases_tac "l" 1);
 by (ALLGOALS Asm_simp_tac);
 by (blast_tac (claset() addIs [less_trans]) 1);
 by (etac ssubst 1);  (*get rid of the needless assumption*)
diff -r 6c6a5410a9bd -r 3c19160b6432 src/HOL/ex/Puzzle.ML
--- a/src/HOL/ex/Puzzle.ML	Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/ex/Puzzle.ML	Mon Mar 13 12:51:10 2000 +0100
@@ -14,7 +14,7 @@
 by (res_inst_tac [("n","k")] less_induct 1);
 by (rtac allI 1);
 by (rename_tac "i" 1);
-by (exhaust_tac "i" 1);
+by (cases_tac "i" 1);
  by (Asm_simp_tac 1);
 by (blast_tac (claset() addSIs [Suc_leI] addIs [le_less_trans]) 1);
 val lemma = result() RS spec RS mp;