exhaust_tac -> cases_tac
authornipkow
Mon Mar 13 12:51:10 2000 +0100 (2000-03-13)
changeset 84233c19160b6432
parent 8422 6c6a5410a9bd
child 8424 a1a41257f45f
exhaust_tac -> cases_tac
src/HOL/Arith.ML
src/HOL/BCV/DFAimpl.ML
src/HOL/BCV/Machine.ML
src/HOL/BCV/Orders.ML
src/HOL/BCV/Orders0.ML
src/HOL/BCV/SemiLattice.ML
src/HOL/BCV/Types0.ML
src/HOL/Finite.ML
src/HOL/Hoare/Examples.ML
src/HOL/IMP/Transition.ML
src/HOL/IOA/IOA.ML
src/HOL/Induct/LList.ML
src/HOL/Integ/Int.ML
src/HOL/Integ/NatBin.ML
src/HOL/Lambda/Eta.ML
src/HOL/Lambda/InductTermi.ML
src/HOL/Lambda/ListBeta.ML
src/HOL/Lambda/ListOrder.ML
src/HOL/Lex/MaxPrefix.ML
src/HOL/Lex/NAe.ML
src/HOL/Lex/Prefix.ML
src/HOL/Lex/RegExp2NA.ML
src/HOL/Lex/RegExp2NAe.ML
src/HOL/Lex/RegSet_of_nat_DA.ML
src/HOL/List.ML
src/HOL/MicroJava/BV/BVSpecTypeSafe.ML
src/HOL/MicroJava/BV/Convert.ML
src/HOL/MicroJava/BV/Correct.ML
src/HOL/MicroJava/BV/LBVComplete.ML
src/HOL/MicroJava/BV/LBVCorrect.ML
src/HOL/MicroJava/BV/LBVSpec.ML
src/HOL/MicroJava/J/JBasis.ML
src/HOL/MicroJava/J/JTypeSafe.ML
src/HOL/MicroJava/J/Type.ML
src/HOL/Nat.ML
src/HOL/Option.ML
src/HOL/Power.ML
src/HOL/Real/RealPow.ML
src/HOL/RelPow.ML
src/HOL/TLA/Inc/Inc.ML
src/HOL/TLA/Memory/Memory.ML
src/HOL/UNITY/GenPrefix.ML
src/HOL/UNITY/Lift_prog.ML
src/HOL/UNITY/TimerArray.ML
src/HOL/UNITY/Token.ML
src/HOL/ex/BinEx.ML
src/HOL/ex/Factorization.ML
src/HOL/ex/Primrec.ML
src/HOL/ex/Puzzle.ML
     1.1 --- a/src/HOL/Arith.ML	Mon Mar 13 12:42:41 2000 +0100
     1.2 +++ b/src/HOL/Arith.ML	Mon Mar 13 12:51:10 2000 +0100
     1.3 @@ -106,24 +106,24 @@
     1.4  (** Reasoning about m+0=0, etc. **)
     1.5  
     1.6  Goal "(m+n = 0) = (m=0 & n=0)";
     1.7 -by (exhaust_tac "m" 1);
     1.8 +by (cases_tac "m" 1);
     1.9  by (Auto_tac);
    1.10  qed "add_is_0";
    1.11  AddIffs [add_is_0];
    1.12  
    1.13  Goal "(0 = m+n) = (m=0 & n=0)";
    1.14 -by (exhaust_tac "m" 1);
    1.15 +by (cases_tac "m" 1);
    1.16  by (Auto_tac);
    1.17  qed "zero_is_add";
    1.18  AddIffs [zero_is_add];
    1.19  
    1.20  Goal "(m+n=1) = (m=1 & n=0 | m=0 & n=1)";
    1.21 -by (exhaust_tac "m" 1);
    1.22 +by (cases_tac "m" 1);
    1.23  by (Auto_tac);
    1.24  qed "add_is_1";
    1.25  
    1.26  Goal "(1=m+n) = (m=1 & n=0 | m=0 & n=1)";
    1.27 -by (exhaust_tac "m" 1);
    1.28 +by (cases_tac "m" 1);
    1.29  by (Auto_tac);
    1.30  qed "one_is_add";
    1.31  
    1.32 @@ -134,7 +134,7 @@
    1.33  
    1.34  (* Could be generalized, eg to "k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
    1.35  Goal "0<n ==> m + (n-1) = (m+n)-1";
    1.36 -by (exhaust_tac "m" 1);
    1.37 +by (cases_tac "m" 1);
    1.38  by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc, Suc_n_not_n]
    1.39                                        addsplits [nat.split])));
    1.40  qed "add_pred";
    1.41 @@ -404,7 +404,7 @@
    1.42  Addsimps [Suc_diff_diff];
    1.43  
    1.44  Goal "0<n ==> n - Suc i < n";
    1.45 -by (exhaust_tac "n" 1);
    1.46 +by (cases_tac "n" 1);
    1.47  by Safe_tac;
    1.48  by (asm_simp_tac (simpset() addsimps le_simps) 1);
    1.49  qed "diff_Suc_less";
    1.50 @@ -1161,16 +1161,16 @@
    1.51  (** Lemmas for ex/Factorization **)
    1.52  
    1.53  Goal "[| 1<n; 1<m |] ==> 1<m*n";
    1.54 -by (exhaust_tac "m" 1);
    1.55 +by (cases_tac "m" 1);
    1.56  by Auto_tac;
    1.57  qed "one_less_mult"; 
    1.58  
    1.59  Goal "[| 1<n; 1<m |] ==> n<m*n";
    1.60 -by (exhaust_tac "m" 1);
    1.61 +by (cases_tac "m" 1);
    1.62  by Auto_tac;
    1.63  qed "n_less_m_mult_n"; 
    1.64  
    1.65  Goal "[| 1<n; 1<m |] ==> n<n*m";
    1.66 -by (exhaust_tac "m" 1);
    1.67 +by (cases_tac "m" 1);
    1.68  by Auto_tac;
    1.69  qed "n_less_n_mult_m"; 
     2.1 --- a/src/HOL/BCV/DFAimpl.ML	Mon Mar 13 12:42:41 2000 +0100
     2.2 +++ b/src/HOL/BCV/DFAimpl.ML	Mon Mar 13 12:51:10 2000 +0100
     2.3 @@ -60,7 +60,7 @@
     2.4       by (Force_tac 2);
     2.5      by (assume_tac 2);
     2.6     by (assume_tac 2);
     2.7 -  by (exhaust_tac "xs!p" 1);
     2.8 +  by (cases_tac "xs!p" 1);
     2.9     by (asm_full_simp_tac (simpset() addsimps [list_update_le_conv]) 1);
    2.10    by (asm_full_simp_tac (simpset() addsimps
    2.11        [list_update_le_conv,listsn_optionE_in]) 1);
    2.12 @@ -147,7 +147,7 @@
    2.13  \         step p s = Some(t) & merges t (succs p) sos = sos))";
    2.14  by (rtac iffI 1);
    2.15   by (asm_simp_tac (simpset() addsimps [next_Some1]) 1);
    2.16 -by (exhaust_tac "next step succs sos" 1);
    2.17 +by (cases_tac "next step succs sos" 1);
    2.18   by (best_tac (claset() addSDs [next_None] addss simpset()) 1);
    2.19  by (rename_tac "sos'" 1);
    2.20  by (case_tac "sos' = sos" 1);
    2.21 @@ -172,7 +172,7 @@
    2.22  \    step_pres_type step n A; succs_bounded succs n;\
    2.23  \    sos : listsn n (option A) |] ==> \
    2.24  \ next step succs sos : option (listsn n (option A))";
    2.25 -by (exhaust_tac "next step succs sos" 1);
    2.26 +by (cases_tac "next step succs sos" 1);
    2.27   by (ALLGOALS Asm_simp_tac);
    2.28  by (rename_tac "sos'" 1);
    2.29  by (case_tac "sos' = sos" 1);
    2.30 @@ -256,7 +256,7 @@
    2.31  by (subgoal_tac
    2.32     "!p<n. !s. sos!p = Some s --> (? u. \
    2.33  \             step p s = Some(u) & (!q:set(succs p). Some u<=tos!q))" 1);
    2.34 - by (exhaust_tac "next step succs sos" 1);
    2.35 + by (cases_tac "next step succs sos" 1);
    2.36    by (dtac next_None 1);
    2.37       by (assume_tac 1);
    2.38      by (assume_tac 1);
    2.39 @@ -279,12 +279,12 @@
    2.40      by (blast_tac (claset() addIs [succs_boundedD,listsn_optionE_in]) 1);
    2.41     by (REPEAT(atac 1));
    2.42  by (Clarify_tac 1);
    2.43 -by (exhaust_tac "tos!p" 1);
    2.44 +by (cases_tac "tos!p" 1);
    2.45   by (force_tac (claset() addDs [le_listD],simpset()) 1);
    2.46  by (rename_tac "t" 1);
    2.47  by (subgoal_tac "s <= t" 1);
    2.48   by (force_tac (claset() addDs [le_listD],simpset()) 2);
    2.49 -by (exhaust_tac "step p s" 1);
    2.50 +by (cases_tac "step p s" 1);
    2.51   by (dtac step_mono_NoneD 1);
    2.52       by (assume_tac 4);
    2.53      by (blast_tac (claset() addIs [listsn_optionE_in]) 1);
     3.1 --- a/src/HOL/BCV/Machine.ML	Mon Mar 13 12:42:41 2000 +0100
     3.2 +++ b/src/HOL/BCV/Machine.ML	Mon Mar 13 12:51:10 2000 +0100
     3.3 @@ -68,15 +68,15 @@
     3.4  by (Blast_tac 2);
     3.5  by (etac thin_rl 1);
     3.6  by (asm_full_simp_tac (simpset() addsimps [le_typ])1);
     3.7 -by (exhaust_tac "t!nat1" 1);
     3.8 +by (cases_tac "t!nat1" 1);
     3.9  by (ALLGOALS Asm_full_simp_tac);
    3.10 -by (exhaust_tac "t!nat2" 1);
    3.11 +by (cases_tac "t!nat2" 1);
    3.12  by (ALLGOALS Asm_full_simp_tac);
    3.13 -by (exhaust_tac "t!nat2" 1);
    3.14 +by (cases_tac "t!nat2" 1);
    3.15  by (ALLGOALS Asm_full_simp_tac);
    3.16 -by (exhaust_tac "s!nat1" 1);
    3.17 +by (cases_tac "s!nat1" 1);
    3.18  by (ALLGOALS Asm_full_simp_tac);
    3.19 -by (exhaust_tac "t!nat2" 1);
    3.20 +by (cases_tac "t!nat2" 1);
    3.21  by (ALLGOALS Asm_full_simp_tac);
    3.22  
    3.23  qed "exec_mono_None";
     4.1 --- a/src/HOL/BCV/Orders.ML	Mon Mar 13 12:42:41 2000 +0100
     4.2 +++ b/src/HOL/BCV/Orders.ML	Mon Mar 13 12:51:10 2000 +0100
     4.3 @@ -37,7 +37,7 @@
     4.4  by (case_tac "? a. Some a : Q" 1);
     4.5   by (eres_inst_tac [("x","{a . Some a : Q}")] allE 1);
     4.6   by (Blast_tac 1);
     4.7 -by (exhaust_tac "x" 1);
     4.8 +by (cases_tac "x" 1);
     4.9   by (Fast_tac 1);
    4.10  by (Blast_tac 1);
    4.11  qed "acc_option";
    4.12 @@ -70,18 +70,18 @@
    4.13   by (Asm_full_simp_tac 1);
    4.14  by (Asm_full_simp_tac 1);
    4.15  by (Clarify_tac 1);
    4.16 -by (exhaust_tac "i" 1);
    4.17 +by (cases_tac "i" 1);
    4.18  by (ALLGOALS Asm_simp_tac);
    4.19  qed "Cons_le_Cons";
    4.20  AddIffs [Cons_le_Cons];
    4.21  
    4.22  Goal "(x#xs <= ys) = (? z zs. ys = z#zs & x <= z & xs <= zs)";
    4.23 -by (exhaust_tac "ys" 1);
    4.24 +by (cases_tac "ys" 1);
    4.25  by (ALLGOALS Asm_simp_tac);
    4.26  qed "Cons_le_iff";
    4.27  
    4.28  Goal "(xs <= y#ys) = (? z zs. xs = z#zs & z <= y & zs <= ys)";
    4.29 -by (exhaust_tac "xs" 1);
    4.30 +by (cases_tac "xs" 1);
    4.31  by (ALLGOALS Asm_simp_tac);
    4.32  qed "le_Cons_iff";
    4.33  
    4.34 @@ -120,7 +120,7 @@
    4.35  
    4.36  Goalw [listsn_def]
    4.37   "(xs : listsn (Suc n) A) = (? y:A. ? ys:listsn n A. xs = y#ys)";
    4.38 -by (exhaust_tac "xs" 1);
    4.39 +by (cases_tac "xs" 1);
    4.40  by (Auto_tac);
    4.41  qed "in_listsn_Suc_iff";
    4.42  
     5.1 --- a/src/HOL/BCV/Orders0.ML	Mon Mar 13 12:42:41 2000 +0100
     5.2 +++ b/src/HOL/BCV/Orders0.ML	Mon Mar 13 12:51:10 2000 +0100
     5.3 @@ -58,11 +58,11 @@
     5.4  by (induct_tac "xs" 1);
     5.5   by (Simp_tac 1);
     5.6  by (rtac allI 1);
     5.7 -by (exhaust_tac "ys" 1);
     5.8 +by (cases_tac "ys" 1);
     5.9   by (hyp_subst_tac 1);
    5.10   by (Simp_tac 1);
    5.11  by (rtac allI 1);
    5.12 -by (exhaust_tac "zs" 1);
    5.13 +by (cases_tac "zs" 1);
    5.14   by (hyp_subst_tac 1);
    5.15   by (Simp_tac 1);
    5.16  by (hyp_subst_tac 1);
    5.17 @@ -87,7 +87,7 @@
    5.18  by (induct_tac "xs" 1);
    5.19   by (Simp_tac 1);
    5.20  by (rtac allI 1);
    5.21 -by (exhaust_tac "ys" 1);
    5.22 +by (cases_tac "ys" 1);
    5.23   by (hyp_subst_tac 1);
    5.24   by (Simp_tac 1);
    5.25  by (hyp_subst_tac 1);
     6.1 --- a/src/HOL/BCV/SemiLattice.ML	Mon Mar 13 12:42:41 2000 +0100
     6.2 +++ b/src/HOL/BCV/SemiLattice.ML	Mon Mar 13 12:51:10 2000 +0100
     6.3 @@ -87,9 +87,9 @@
     6.4  by (induct_tac "n" 1);
     6.5   by (Simp_tac 1);
     6.6  by (Clarify_tac 1);
     6.7 -by (exhaust_tac "xs" 1);
     6.8 +by (cases_tac "xs" 1);
     6.9   by (Asm_full_simp_tac 1);
    6.10 -by (exhaust_tac "ys" 1);
    6.11 +by (cases_tac "ys" 1);
    6.12   by (Asm_full_simp_tac 1);
    6.13  by (asm_full_simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1);
    6.14  qed_spec_mp "nth_plus";
    6.15 @@ -123,9 +123,9 @@
    6.16   by (Simp_tac 1);
    6.17  by (Asm_full_simp_tac 1);
    6.18  by (Clarify_tac 1);
    6.19 -by (exhaust_tac "xs" 1);
    6.20 +by (cases_tac "xs" 1);
    6.21   by (Asm_full_simp_tac 1);
    6.22 -by (exhaust_tac "ys" 1);
    6.23 +by (cases_tac "ys" 1);
    6.24   by (Asm_full_simp_tac 1);
    6.25  by (Asm_full_simp_tac 1);
    6.26  by (blast_tac (claset() addIs [semilat_plus]) 1);
     7.1 --- a/src/HOL/BCV/Types0.ML	Mon Mar 13 12:42:41 2000 +0100
     7.2 +++ b/src/HOL/BCV/Types0.ML	Mon Mar 13 12:51:10 2000 +0100
     7.3 @@ -23,7 +23,7 @@
     7.4  Goal "(UNIV::typ set) = {Atyp,Btyp,Ctyp,Top}";
     7.5  by (Auto_tac);
     7.6  by (rename_tac "t" 1);
     7.7 -by (exhaust_tac "t" 1);
     7.8 +by (cases_tac "t" 1);
     7.9  by (Auto_tac);
    7.10  qed "UNIV_typ_enum";
    7.11  
     8.1 --- a/src/HOL/Finite.ML	Mon Mar 13 12:42:41 2000 +0100
     8.2 +++ b/src/HOL/Finite.ML	Mon Mar 13 12:51:10 2000 +0100
     8.3 @@ -248,7 +248,7 @@
     8.4  
     8.5  Goal "[| x ~: A; insert x A = {f i|i. i<n} |]  \
     8.6  \     ==> ? m::nat. m<n & (? g. A = {g i|i. i<m})";
     8.7 -by (exhaust_tac "n" 1);
     8.8 +by (cases_tac "n" 1);
     8.9   by (hyp_subst_tac 1);
    8.10   by (Asm_full_simp_tac 1);
    8.11  by (rename_tac "m" 1);
     9.1 --- a/src/HOL/Hoare/Examples.ML	Mon Mar 13 12:42:41 2000 +0100
     9.2 +++ b/src/HOL/Hoare/Examples.ML	Mon Mar 13 12:51:10 2000 +0100
     9.3 @@ -50,7 +50,7 @@
     9.4  \ OD \
     9.5  \ {c = A^B}";
     9.6  by (hoare_tac (Asm_full_simp_tac) 1);
     9.7 -by (exhaust_tac "b" 1);
     9.8 +by (cases_tac "b" 1);
     9.9  by (hyp_subst_tac 1);
    9.10  by (asm_full_simp_tac (simpset() addsimps [mod_less]) 1);
    9.11  by (asm_simp_tac (simpset() addsimps [mult_assoc]) 1);
    9.12 @@ -67,7 +67,7 @@
    9.13  \ {b = fac A}";
    9.14  by (hoare_tac Asm_full_simp_tac 1);
    9.15  by (Clarify_tac 1);
    9.16 -by (exhaust_tac "a" 1);
    9.17 +by (cases_tac "a" 1);
    9.18  by (ALLGOALS
    9.19      (asm_simp_tac
    9.20       (simpset() addsimps [add_mult_distrib,add_mult_distrib2,mult_assoc])));
    10.1 --- a/src/HOL/IMP/Transition.ML	Mon Mar 13 12:42:41 2000 +0100
    10.2 +++ b/src/HOL/IMP/Transition.ML	Mon Mar 13 12:51:10 2000 +0100
    10.3 @@ -220,7 +220,7 @@
    10.4  by (Clarify_tac 1);
    10.5  by (etac rel_pow_E2 1);
    10.6   by (asm_full_simp_tac (simpset() addsimps evalc.intrs) 1);
    10.7 -by (exhaust_tac "c" 1);
    10.8 +by (cases_tac "c" 1);
    10.9      by (fast_tac (claset() addSDs [hlemma]) 1);
   10.10     by (Blast_tac 1);
   10.11    by (blast_tac (claset() addSDs [rel_pow_Suc_I2 RS comp_decomp_lemma]) 1);
    11.1 --- a/src/HOL/IOA/IOA.ML	Mon Mar 13 12:42:41 2000 +0100
    11.2 +++ b/src/HOL/IOA/IOA.ML	Mon Mar 13 12:51:10 2000 +0100
    11.3 @@ -30,7 +30,7 @@
    11.4  Goal "filter_oseq p (filter_oseq p s) = filter_oseq p s";
    11.5    by (simp_tac (simpset() addsimps [filter_oseq_def]) 1);
    11.6    by (rtac ext 1);
    11.7 -  by (exhaust_tac "s(i)" 1);
    11.8 +  by (cases_tac "s(i)" 1);
    11.9    by (Asm_simp_tac 1);
   11.10    by (Asm_simp_tac 1);
   11.11  qed "filter_oseq_idemp";
   11.12 @@ -41,7 +41,7 @@
   11.13  \  &                                                              \
   11.14  \  (mk_trace A s n = Some(a)) =                                   \
   11.15  \   (s(n)=Some(a) & a : externals(asig_of(A)))";
   11.16 -  by (exhaust_tac "s(n)" 1);
   11.17 +  by (cases_tac "s(n)" 1);
   11.18    by (ALLGOALS Asm_simp_tac);
   11.19    by (Fast_tac 1);
   11.20  qed "mk_trace_thm";
   11.21 @@ -86,7 +86,7 @@
   11.22    by (induct_tac "n" 1);
   11.23     by (fast_tac (claset() addIs [p1,reachable_0]) 1);
   11.24    by (eres_inst_tac[("x","na")] allE 1);
   11.25 -  by (exhaust_tac "ex1 na" 1 THEN ALLGOALS Asm_full_simp_tac);
   11.26 +  by (cases_tac "ex1 na" 1 THEN ALLGOALS Asm_full_simp_tac);
   11.27    by Safe_tac;
   11.28     by (etac (p2 RS mp) 1);
   11.29      by (ALLGOALS(fast_tac(claset() addDs [reachable_n])));
    12.1 --- a/src/HOL/Induct/LList.ML	Mon Mar 13 12:42:41 2000 +0100
    12.2 +++ b/src/HOL/Induct/LList.ML	Mon Mar 13 12:51:10 2000 +0100
    12.3 @@ -76,7 +76,7 @@
    12.4      "LList_corec a f <= \
    12.5  \    (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))";
    12.6  by (rtac UN_least 1);
    12.7 -by (exhaust_tac "k" 1);
    12.8 +by (cases_tac "k" 1);
    12.9  by (ALLGOALS Asm_simp_tac);
   12.10  by (REPEAT (resolve_tac [allI, impI, subset_refl RS CONS_mono, 
   12.11  			 UNIV_I RS UN_upper] 1));
   12.12 @@ -132,10 +132,10 @@
   12.13  by (safe_tac (claset() delrules [equalityI]));
   12.14  by (etac LListD.elim 1);
   12.15  by (safe_tac (claset() delrules [equalityI]));
   12.16 -by (exhaust_tac "n" 1);
   12.17 +by (cases_tac "n" 1);
   12.18  by (Asm_simp_tac 1);
   12.19  by (rename_tac "n'" 1);
   12.20 -by (exhaust_tac "n'" 1);
   12.21 +by (cases_tac "n'" 1);
   12.22  by (asm_simp_tac (simpset() addsimps [CONS_def]) 1);
   12.23  by (asm_simp_tac (simpset() addsimps [CONS_def, less_Suc_eq]) 1);
   12.24  qed "LListD_implies_ntrunc_equality";
   12.25 @@ -295,9 +295,9 @@
   12.26  by (stac prem2 1);
   12.27  by (Simp_tac 1);
   12.28  by (strip_tac 1);
   12.29 -by (exhaust_tac "n" 1);
   12.30 +by (cases_tac "n" 1);
   12.31  by (rename_tac "m" 2);
   12.32 -by (exhaust_tac "m" 2);
   12.33 +by (cases_tac "m" 2);
   12.34  by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
   12.35  result();
   12.36  
   12.37 @@ -598,7 +598,7 @@
   12.38      "llist_corec a f =  \
   12.39  \    (case f a of None => LNil | Some(z,w) => LCons z (llist_corec w f))";
   12.40  by (stac LList_corec 1);
   12.41 -by (exhaust_tac "f a" 1);
   12.42 +by (cases_tac "f a" 1);
   12.43  by (asm_simp_tac (simpset() addsimps [LList_corec_type2]) 1);
   12.44  by (force_tac (claset(), simpset() addsimps [LList_corec_type2]) 1);
   12.45  qed "llist_corec";
    13.1 --- a/src/HOL/Integ/Int.ML	Mon Mar 13 12:42:41 2000 +0100
    13.2 +++ b/src/HOL/Integ/Int.ML	Mon Mar 13 12:51:10 2000 +0100
    13.3 @@ -90,7 +90,7 @@
    13.4  by (cut_inst_tac [("m","m")] int_Suc_int_1 1);
    13.5  by (cut_inst_tac [("m","n")] int_Suc_int_1 1);
    13.6  by (Asm_full_simp_tac 1);
    13.7 -by (exhaust_tac "n" 1);
    13.8 +by (cases_tac "n" 1);
    13.9  by Auto_tac;
   13.10  by (cut_inst_tac [("m","m")] int_Suc_int_1 1);
   13.11  by (full_simp_tac (simpset() addsimps zadd_ac) 1);
    14.1 --- a/src/HOL/Integ/NatBin.ML	Mon Mar 13 12:42:41 2000 +0100
    14.2 +++ b/src/HOL/Integ/NatBin.ML	Mon Mar 13 12:51:10 2000 +0100
    14.3 @@ -319,17 +319,17 @@
    14.4  (* These two can be useful when m = number_of... *)
    14.5  
    14.6  Goal "(m::nat) + n = (if m=#0 then n else Suc ((m - #1) + n))";
    14.7 -by (exhaust_tac "m" 1);
    14.8 +by (cases_tac "m" 1);
    14.9  by (ALLGOALS (asm_simp_tac numeral_ss));
   14.10  qed "add_eq_if";
   14.11  
   14.12  Goal "(m::nat) * n = (if m=#0 then #0 else n + ((m - #1) * n))";
   14.13 -by (exhaust_tac "m" 1);
   14.14 +by (cases_tac "m" 1);
   14.15  by (ALLGOALS (asm_simp_tac numeral_ss));
   14.16  qed "mult_eq_if";
   14.17  
   14.18  Goal "(p ^ m :: nat) = (if m=#0 then #1 else p * (p ^ (m - #1)))";
   14.19 -by (exhaust_tac "m" 1);
   14.20 +by (cases_tac "m" 1);
   14.21  by (ALLGOALS (asm_simp_tac numeral_ss));
   14.22  qed "power_eq_if";
   14.23  
    15.1 --- a/src/HOL/Lambda/Eta.ML	Mon Mar 13 12:42:41 2000 +0100
    15.2 +++ b/src/HOL/Lambda/Eta.ML	Mon Mar 13 12:51:10 2000 +0100
    15.3 @@ -166,7 +166,7 @@
    15.4    by (rtac notE 1);
    15.5     by (assume_tac 2);
    15.6    by (etac thin_rl 1);
    15.7 -  by (exhaust_tac "t" 1);
    15.8 +  by (cases_tac "t" 1);
    15.9      by (Asm_simp_tac 1);
   15.10     by (Asm_simp_tac 1);
   15.11    by (Asm_simp_tac 1);
   15.12 @@ -181,7 +181,7 @@
   15.13    by (Asm_simp_tac 1);
   15.14   by (etac exE 1);
   15.15   by (etac rev_mp 1);
   15.16 - by (exhaust_tac "t" 1);
   15.17 + by (cases_tac "t" 1);
   15.18     by (Asm_simp_tac 1);
   15.19    by (Asm_simp_tac 1);
   15.20    by (Blast_tac 1);
   15.21 @@ -195,7 +195,7 @@
   15.22   by (Asm_simp_tac 1);
   15.23  by (etac exE 1);
   15.24  by (etac rev_mp 1);
   15.25 -by (exhaust_tac "t" 1);
   15.26 +by (cases_tac "t" 1);
   15.27    by (Asm_simp_tac 1);
   15.28   by (Asm_simp_tac 1);
   15.29  by (Asm_simp_tac 1);
    16.1 --- a/src/HOL/Lambda/InductTermi.ML	Mon Mar 13 12:42:41 2000 +0100
    16.2 +++ b/src/HOL/Lambda/InductTermi.ML	Mon Mar 13 12:51:10 2000 +0100
    16.3 @@ -86,7 +86,7 @@
    16.4    by (eres_inst_tac [("x","Var n $$ us")] allE 1);
    16.5    by (Force_tac 1);
    16.6  by (rename_tac "u ts" 1);
    16.7 -by (exhaust_tac "ts" 1);
    16.8 +by (cases_tac "ts" 1);
    16.9   by (Asm_full_simp_tac 1);
   16.10   by (blast_tac (claset() addIs IT.intrs) 1);
   16.11  by (rename_tac "s ss" 1);
    17.1 --- a/src/HOL/Lambda/ListBeta.ML	Mon Mar 13 12:42:41 2000 +0100
    17.2 +++ b/src/HOL/Lambda/ListBeta.ML	Mon Mar 13 12:51:10 2000 +0100
    17.3 @@ -29,7 +29,7 @@
    17.4  \       (? s t ts. r = Abs s & rs = t#ts & u' = s[t/0]$$ts))";
    17.5  by (etac beta.induct 1);
    17.6     by (clarify_tac (claset() delrules [disjCI]) 1);
    17.7 -   by (exhaust_tac "r" 1);
    17.8 +   by (cases_tac "r" 1);
    17.9       by (Asm_full_simp_tac 1);
   17.10      by (asm_full_simp_tac (simpset() addsimps [App_eq_foldl_conv]) 1);
   17.11      by (split_asm_tac [split_if_asm] 1);
    18.1 --- a/src/HOL/Lambda/ListOrder.ML	Mon Mar 13 12:42:41 2000 +0100
    18.2 +++ b/src/HOL/Lambda/ListOrder.ML	Mon Mar 13 12:51:10 2000 +0100
    18.3 @@ -30,7 +30,7 @@
    18.4  by (rtac iffI 1);
    18.5   by (etac exE 1);
    18.6   by (rename_tac "ts" 1);
    18.7 - by (exhaust_tac "ts" 1);
    18.8 + by (cases_tac "ts" 1);
    18.9    by (Force_tac 1);
   18.10   by (Force_tac 1);
   18.11  by (etac disjE 1);
   18.12 @@ -51,7 +51,7 @@
   18.13  \        !y. ys = y#xs --> (y,x) : r --> R; \
   18.14  \        !zs. ys = x#zs --> (zs,xs) : step1 r --> R \
   18.15  \     |] ==> R";
   18.16 -by (exhaust_tac "ys" 1);
   18.17 +by (cases_tac "ys" 1);
   18.18   by (asm_full_simp_tac (simpset() addsimps [step1_def]) 1);
   18.19  by (Blast_tac 1);
   18.20  val lemma = result();
    19.1 --- a/src/HOL/Lex/MaxPrefix.ML	Mon Mar 13 12:42:41 2000 +0100
    19.2 +++ b/src/HOL/Lex/MaxPrefix.ML	Mon Mar 13 12:51:10 2000 +0100
    19.3 @@ -26,7 +26,7 @@
    19.4  by (case_tac "? us. us <= a#list & P (ps @ us)" 1);
    19.5   by (Asm_simp_tac 1);
    19.6   by (Clarify_tac 1);
    19.7 - by (exhaust_tac "us" 1);
    19.8 + by (cases_tac "us" 1);
    19.9    by (rtac iffI 1);
   19.10     by (asm_full_simp_tac (simpset() addsimps [prefix_Cons,prefix_append]) 1);
   19.11     by (Blast_tac 1);
    20.1 --- a/src/HOL/Lex/NAe.ML	Mon Mar 13 12:42:41 2000 +0100
    20.2 +++ b/src/HOL/Lex/NAe.ML	Mon Mar 13 12:51:10 2000 +0100
    20.3 @@ -5,7 +5,7 @@
    20.4  *)
    20.5  
    20.6  Goal "steps A w O (eps A)^* = steps A w";
    20.7 -by (exhaust_tac "w" 1);
    20.8 +by (cases_tac "w" 1);
    20.9  by (ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
   20.10  qed_spec_mp "steps_epsclosure";
   20.11  Addsimps [steps_epsclosure];
    21.1 --- a/src/HOL/Lex/Prefix.ML	Mon Mar 13 12:42:41 2000 +0100
    21.2 +++ b/src/HOL/Lex/Prefix.ML	Mon Mar 13 12:51:10 2000 +0100
    21.3 @@ -76,7 +76,7 @@
    21.4  
    21.5  Goalw [prefix_def]
    21.6     "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
    21.7 -by (exhaust_tac "xs" 1);
    21.8 +by (cases_tac "xs" 1);
    21.9  by Auto_tac;
   21.10  qed "prefix_Cons";
   21.11  
   21.12 @@ -92,7 +92,7 @@
   21.13  Goalw [prefix_def]
   21.14    "[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys";
   21.15  by (auto_tac(claset(), simpset() addsimps [nth_append]));
   21.16 -by (exhaust_tac "ys" 1);
   21.17 +by (cases_tac "ys" 1);
   21.18  by Auto_tac;
   21.19  qed "append_one_prefix";
   21.20  
    22.1 --- a/src/HOL/Lex/RegExp2NA.ML	Mon Mar 13 12:42:41 2000 +0100
    22.2 +++ b/src/HOL/Lex/RegExp2NA.ML	Mon Mar 13 12:51:10 2000 +0100
    22.3 @@ -112,7 +112,7 @@
    22.4  \ ( (w = [] & q = start(union L R)) | \
    22.5  \   (w ~= [] & (? p.  q = True  # p & (start L,p) : steps L w | \
    22.6  \                     q = False # p & (start R,p) : steps R w)))";
    22.7 -by (exhaust_tac "w" 1);
    22.8 +by (cases_tac "w" 1);
    22.9   by (Asm_simp_tac 1);
   22.10   by (Blast_tac 1);
   22.11  by (Asm_simp_tac 1);
   22.12 @@ -273,7 +273,7 @@
   22.13   by (Simp_tac 1);
   22.14   by (Blast_tac 1);
   22.15  by (Clarify_tac 1);
   22.16 -by (exhaust_tac "v" 1);
   22.17 +by (cases_tac "v" 1);
   22.18   by (Asm_full_simp_tac 1);
   22.19   by (Blast_tac 1);
   22.20  by (Asm_full_simp_tac 1);
   22.21 @@ -336,7 +336,7 @@
   22.22  Goal
   22.23   "[| (start A,q) : steps A u; u ~= []; fin A p |] \
   22.24  \ ==> (p,q) : steps (plus A) u";
   22.25 -by (exhaust_tac "u" 1);
   22.26 +by (cases_tac "u" 1);
   22.27   by (Blast_tac 1);
   22.28  by (Asm_full_simp_tac 1);
   22.29  by (blast_tac (claset() addIs [steps_plusI]) 1);
   22.30 @@ -360,7 +360,7 @@
   22.31   by (res_inst_tac [("x","us")] exI 1);
   22.32   by (Asm_simp_tac 1);
   22.33   by (Blast_tac 1);
   22.34 -by (exhaust_tac "v" 1);
   22.35 +by (cases_tac "v" 1);
   22.36   by (res_inst_tac [("x","us")] exI 1);
   22.37   by (Asm_full_simp_tac 1);
   22.38  by (res_inst_tac [("x","us@[v]")] exI 1);
    23.1 --- a/src/HOL/Lex/RegExp2NAe.ML	Mon Mar 13 12:42:41 2000 +0100
    23.2 +++ b/src/HOL/Lex/RegExp2NAe.ML	Mon Mar 13 12:51:10 2000 +0100
    23.3 @@ -191,7 +191,7 @@
    23.4  \ ( (w = [] & q = start(union L R)) | \
    23.5  \   (? p.  q = True  # p & (start L,p) : steps L w | \
    23.6  \          q = False # p & (start R,p) : steps R w) )";
    23.7 -by (exhaust_tac "w" 1);
    23.8 +by (cases_tac "w" 1);
    23.9   by (Asm_simp_tac 1);
   23.10   by (Blast_tac 1);
   23.11  by (Asm_simp_tac 1);
   23.12 @@ -568,7 +568,7 @@
   23.13   "(start(star A),r) : steps (star A) w = \
   23.14  \ ((w=[] & r= start(star A)) | (True#start A,r) : steps (star A) w)";
   23.15  by (rtac iffI 1);
   23.16 - by (exhaust_tac "w" 1);
   23.17 + by (cases_tac "w" 1);
   23.18    by (asm_full_simp_tac (simpset() addsimps
   23.19      [epsclosure_start_step_star]) 1);
   23.20   by (Asm_full_simp_tac 1);
    24.1 --- a/src/HOL/Lex/RegSet_of_nat_DA.ML	Mon Mar 13 12:42:41 2000 +0100
    24.2 +++ b/src/HOL/Lex/RegSet_of_nat_DA.ML	Mon Mar 13 12:51:10 2000 +0100
    24.3 @@ -11,7 +11,7 @@
    24.4  (* Lists *)
    24.5  
    24.6  Goal "(butlast xs = []) = (case xs of [] => True | y#ys => ys=[])";
    24.7 -by (exhaust_tac "xs" 1);
    24.8 +by (cases_tac "xs" 1);
    24.9  by (ALLGOALS Asm_simp_tac);
   24.10  qed "butlast_empty";
   24.11  AddIffs [butlast_empty];
   24.12 @@ -103,14 +103,14 @@
   24.13  Addsimps [trace_concat];
   24.14  
   24.15  Goal "!i. (trace d i xs = []) = (xs = [])";
   24.16 -by (exhaust_tac "xs" 1);
   24.17 +by (cases_tac "xs" 1);
   24.18  by (ALLGOALS Asm_simp_tac);
   24.19  qed "trace_is_Nil";
   24.20  Addsimps [trace_is_Nil];
   24.21  
   24.22  Goal "(trace d i xs = n#ns) = \
   24.23  \         (case xs of [] => False | y#ys => n = d y i & ns = trace d n ys)";
   24.24 -by (exhaust_tac "xs" 1);
   24.25 +by (cases_tac "xs" 1);
   24.26  by (ALLGOALS Asm_simp_tac);
   24.27  by (Blast_tac 1);
   24.28  qed_spec_mp "trace_is_Cons_conv";
    25.1 --- a/src/HOL/List.ML	Mon Mar 13 12:42:41 2000 +0100
    25.2 +++ b/src/HOL/List.ML	Mon Mar 13 12:51:10 2000 +0100
    25.3 @@ -88,7 +88,7 @@
    25.4  Addsimps [length_rev];
    25.5  
    25.6  Goal "length(tl xs) = (length xs) - 1";
    25.7 -by (exhaust_tac "xs" 1);
    25.8 +by (cases_tac "xs" 1);
    25.9  by Auto_tac;
   25.10  qed "length_tl";
   25.11  Addsimps [length_tl];
   25.12 @@ -159,11 +159,11 @@
   25.13  \              --> (xs@us = ys@vs) = (xs=ys & us=vs)";
   25.14  by (induct_tac "xs" 1);
   25.15   by (rtac allI 1);
   25.16 - by (exhaust_tac "ys" 1);
   25.17 + by (cases_tac "ys" 1);
   25.18    by (Asm_simp_tac 1);
   25.19   by (Force_tac 1);
   25.20  by (rtac allI 1);
   25.21 -by (exhaust_tac "ys" 1);
   25.22 +by (cases_tac "ys" 1);
   25.23  by (Force_tac 1);
   25.24  by (Asm_simp_tac 1);
   25.25  qed_spec_mp "append_eq_append_conv";
   25.26 @@ -340,19 +340,19 @@
   25.27  bind_thm("map_cong", impI RSN (2,allI RSN (2, result() RS mp)));
   25.28  
   25.29  Goal "(map f xs = []) = (xs = [])";
   25.30 -by (exhaust_tac "xs" 1);
   25.31 +by (cases_tac "xs" 1);
   25.32  by Auto_tac;
   25.33  qed "map_is_Nil_conv";
   25.34  AddIffs [map_is_Nil_conv];
   25.35  
   25.36  Goal "([] = map f xs) = (xs = [])";
   25.37 -by (exhaust_tac "xs" 1);
   25.38 +by (cases_tac "xs" 1);
   25.39  by Auto_tac;
   25.40  qed "Nil_is_map_conv";
   25.41  AddIffs [Nil_is_map_conv];
   25.42  
   25.43  Goal "(map f xs = y#ys) = (? x xs'. xs = x#xs' & f x = y & map f xs' = ys)";
   25.44 -by (exhaust_tac "xs" 1);
   25.45 +by (cases_tac "xs" 1);
   25.46  by (ALLGOALS Asm_simp_tac);
   25.47  qed "map_eq_Cons";
   25.48  
   25.49 @@ -411,7 +411,7 @@
   25.50  by (induct_tac "xs" 1);
   25.51   by (Force_tac 1);
   25.52  by (rtac allI 1);
   25.53 -by (exhaust_tac "ys" 1);
   25.54 +by (cases_tac "ys" 1);
   25.55   by (Asm_simp_tac 1);
   25.56  by (Force_tac 1);
   25.57  qed_spec_mp "rev_is_rev_conv";
   25.58 @@ -492,7 +492,7 @@
   25.59  by (rtac iffI 1);
   25.60  by (blast_tac (claset() addIs [eq_Nil_appendI,Cons_eq_appendI]) 1);
   25.61  by (REPEAT(etac exE 1));
   25.62 -by (exhaust_tac "ys" 1);
   25.63 +by (cases_tac "ys" 1);
   25.64  by Auto_tac;
   25.65  qed "in_set_conv_decomp";
   25.66  
   25.67 @@ -630,7 +630,7 @@
   25.68  by (induct_tac "xs" 1);
   25.69   by (Asm_simp_tac 1);
   25.70   by (rtac allI 1);
   25.71 - by (exhaust_tac "n" 1);
   25.72 + by (cases_tac "n" 1);
   25.73    by Auto_tac;
   25.74  qed_spec_mp "nth_append";
   25.75  
   25.76 @@ -652,7 +652,7 @@
   25.77    by (Simp_tac 1);
   25.78   by (res_inst_tac [("x","Suc i")] exI 1);
   25.79   by (Asm_simp_tac 1);
   25.80 -by (exhaust_tac "i" 1);
   25.81 +by (cases_tac "i" 1);
   25.82   by (Asm_full_simp_tac 1);
   25.83  by (rename_tac "j" 1);
   25.84   by (res_inst_tac [("x","j")] exI 1);
   25.85 @@ -728,7 +728,7 @@
   25.86  \     (zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])";
   25.87  by (induct_tac "ys" 1);
   25.88   by Auto_tac;
   25.89 -by (exhaust_tac "xs" 1);
   25.90 +by (cases_tac "xs" 1);
   25.91   by (auto_tac (claset(), simpset() addsplits [nat.split]));
   25.92  qed_spec_mp "update_zip";
   25.93  
   25.94 @@ -813,7 +813,7 @@
   25.95  Goal "!xs. length(take n xs) = min (length xs) n";
   25.96  by (induct_tac "n" 1);
   25.97   by Auto_tac;
   25.98 -by (exhaust_tac "xs" 1);
   25.99 +by (cases_tac "xs" 1);
  25.100   by Auto_tac;
  25.101  qed_spec_mp "length_take";
  25.102  Addsimps [length_take];
  25.103 @@ -821,7 +821,7 @@
  25.104  Goal "!xs. length(drop n xs) = (length xs - n)";
  25.105  by (induct_tac "n" 1);
  25.106   by Auto_tac;
  25.107 -by (exhaust_tac "xs" 1);
  25.108 +by (cases_tac "xs" 1);
  25.109   by Auto_tac;
  25.110  qed_spec_mp "length_drop";
  25.111  Addsimps [length_drop];
  25.112 @@ -829,7 +829,7 @@
  25.113  Goal "!xs. length xs <= n --> take n xs = xs";
  25.114  by (induct_tac "n" 1);
  25.115   by Auto_tac;
  25.116 -by (exhaust_tac "xs" 1);
  25.117 +by (cases_tac "xs" 1);
  25.118   by Auto_tac;
  25.119  qed_spec_mp "take_all";
  25.120  Addsimps [take_all];
  25.121 @@ -837,7 +837,7 @@
  25.122  Goal "!xs. length xs <= n --> drop n xs = []";
  25.123  by (induct_tac "n" 1);
  25.124   by Auto_tac;
  25.125 -by (exhaust_tac "xs" 1);
  25.126 +by (cases_tac "xs" 1);
  25.127   by Auto_tac;
  25.128  qed_spec_mp "drop_all";
  25.129  Addsimps [drop_all];
  25.130 @@ -845,7 +845,7 @@
  25.131  Goal "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
  25.132  by (induct_tac "n" 1);
  25.133   by Auto_tac;
  25.134 -by (exhaust_tac "xs" 1);
  25.135 +by (cases_tac "xs" 1);
  25.136   by Auto_tac;
  25.137  qed_spec_mp "take_append";
  25.138  Addsimps [take_append];
  25.139 @@ -853,7 +853,7 @@
  25.140  Goal "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys"; 
  25.141  by (induct_tac "n" 1);
  25.142   by Auto_tac;
  25.143 -by (exhaust_tac "xs" 1);
  25.144 +by (cases_tac "xs" 1);
  25.145   by Auto_tac;
  25.146  qed_spec_mp "drop_append";
  25.147  Addsimps [drop_append];
  25.148 @@ -861,9 +861,9 @@
  25.149  Goal "!xs n. take n (take m xs) = take (min n m) xs"; 
  25.150  by (induct_tac "m" 1);
  25.151   by Auto_tac;
  25.152 -by (exhaust_tac "xs" 1);
  25.153 +by (cases_tac "xs" 1);
  25.154   by Auto_tac;
  25.155 -by (exhaust_tac "na" 1);
  25.156 +by (cases_tac "na" 1);
  25.157   by Auto_tac;
  25.158  qed_spec_mp "take_take";
  25.159  Addsimps [take_take];
  25.160 @@ -871,7 +871,7 @@
  25.161  Goal "!xs. drop n (drop m xs) = drop (n + m) xs"; 
  25.162  by (induct_tac "m" 1);
  25.163   by Auto_tac;
  25.164 -by (exhaust_tac "xs" 1);
  25.165 +by (cases_tac "xs" 1);
  25.166   by Auto_tac;
  25.167  qed_spec_mp "drop_drop";
  25.168  Addsimps [drop_drop];
  25.169 @@ -879,14 +879,14 @@
  25.170  Goal "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; 
  25.171  by (induct_tac "m" 1);
  25.172   by Auto_tac;
  25.173 -by (exhaust_tac "xs" 1);
  25.174 +by (cases_tac "xs" 1);
  25.175   by Auto_tac;
  25.176  qed_spec_mp "take_drop";
  25.177  
  25.178  Goal "!xs. take n xs @ drop n xs = xs";
  25.179  by (induct_tac "n" 1);
  25.180   by Auto_tac;
  25.181 -by (exhaust_tac "xs" 1);
  25.182 +by (cases_tac "xs" 1);
  25.183   by Auto_tac;
  25.184  qed_spec_mp "append_take_drop_id";
  25.185  Addsimps [append_take_drop_id];
  25.186 @@ -894,23 +894,23 @@
  25.187  Goal "!xs. take n (map f xs) = map f (take n xs)"; 
  25.188  by (induct_tac "n" 1);
  25.189   by Auto_tac;
  25.190 -by (exhaust_tac "xs" 1);
  25.191 +by (cases_tac "xs" 1);
  25.192   by Auto_tac;
  25.193  qed_spec_mp "take_map"; 
  25.194  
  25.195  Goal "!xs. drop n (map f xs) = map f (drop n xs)"; 
  25.196  by (induct_tac "n" 1);
  25.197   by Auto_tac;
  25.198 -by (exhaust_tac "xs" 1);
  25.199 +by (cases_tac "xs" 1);
  25.200   by Auto_tac;
  25.201  qed_spec_mp "drop_map";
  25.202  
  25.203  Goal "!n i. i < n --> (take n xs)!i = xs!i";
  25.204  by (induct_tac "xs" 1);
  25.205   by Auto_tac;
  25.206 -by (exhaust_tac "n" 1);
  25.207 +by (cases_tac "n" 1);
  25.208   by (Blast_tac 1);
  25.209 -by (exhaust_tac "i" 1);
  25.210 +by (cases_tac "i" 1);
  25.211   by Auto_tac;
  25.212  qed_spec_mp "nth_take";
  25.213  Addsimps [nth_take];
  25.214 @@ -918,7 +918,7 @@
  25.215  Goal  "!xs i. n + i <= length xs --> (drop n xs)!i = xs!(n+i)";
  25.216  by (induct_tac "n" 1);
  25.217   by Auto_tac;
  25.218 -by (exhaust_tac "xs" 1);
  25.219 +by (cases_tac "xs" 1);
  25.220   by Auto_tac;
  25.221  qed_spec_mp "nth_drop";
  25.222  Addsimps [nth_drop];
  25.223 @@ -930,7 +930,7 @@
  25.224   by (Simp_tac 1);
  25.225  by (Asm_full_simp_tac 1);
  25.226  by (Clarify_tac 1);
  25.227 -by (exhaust_tac "zs" 1);
  25.228 +by (cases_tac "zs" 1);
  25.229  by (Auto_tac);
  25.230  qed_spec_mp "append_eq_conv_conj";
  25.231  
  25.232 @@ -993,7 +993,7 @@
  25.233  by (induct_tac "ys" 1);
  25.234   by (Simp_tac 1);
  25.235  by (Clarify_tac 1);
  25.236 -by (exhaust_tac "xs" 1);
  25.237 +by (cases_tac "xs" 1);
  25.238   by (Auto_tac);
  25.239  qed_spec_mp "length_zip";
  25.240  Addsimps [length_zip];
  25.241 @@ -1004,7 +1004,7 @@
  25.242  by (induct_tac "zs" 1);
  25.243   by (Simp_tac 1);
  25.244  by (Clarify_tac 1);
  25.245 -by (exhaust_tac "xs" 1);
  25.246 +by (cases_tac "xs" 1);
  25.247   by (Asm_simp_tac 1);
  25.248  by (Asm_simp_tac 1);
  25.249  qed_spec_mp "zip_append1";
  25.250 @@ -1015,7 +1015,7 @@
  25.251  by (induct_tac "xs" 1);
  25.252   by (Simp_tac 1);
  25.253  by (Clarify_tac 1);
  25.254 -by (exhaust_tac "ys" 1);
  25.255 +by (cases_tac "ys" 1);
  25.256   by (Asm_simp_tac 1);
  25.257  by (Asm_simp_tac 1);
  25.258  qed_spec_mp "zip_append2";
  25.259 @@ -1032,7 +1032,7 @@
  25.260   by (Asm_full_simp_tac 1);
  25.261  by (Asm_full_simp_tac 1);
  25.262  by (Clarify_tac 1);
  25.263 -by (exhaust_tac "xs" 1);
  25.264 +by (cases_tac "xs" 1);
  25.265   by (Auto_tac);
  25.266  qed_spec_mp "zip_rev";
  25.267  
  25.268 @@ -1042,7 +1042,7 @@
  25.269  by (induct_tac "ys" 1);
  25.270   by (Simp_tac 1);
  25.271  by (Clarify_tac 1);
  25.272 -by (exhaust_tac "xs" 1);
  25.273 +by (cases_tac "xs" 1);
  25.274   by (Auto_tac);
  25.275  by (asm_full_simp_tac (simpset() addsimps (thms"nth.simps") addsplits [nat.split]) 1);
  25.276  qed_spec_mp "nth_zip";
  25.277 @@ -1061,7 +1061,7 @@
  25.278  Goal "!j. zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)";
  25.279  by (induct_tac "i" 1);
  25.280   by (Auto_tac);
  25.281 -by (exhaust_tac "j" 1);
  25.282 +by (cases_tac "j" 1);
  25.283   by (Auto_tac);
  25.284  qed "zip_replicate";
  25.285  Addsimps [zip_replicate];
  25.286 @@ -1091,13 +1091,13 @@
  25.287  
  25.288  Goalw [list_all2_def]
  25.289   "list_all2 P (x#xs) ys = (? z zs. ys = z#zs & P x z & list_all2 P xs zs)";
  25.290 -by (exhaust_tac "ys" 1);
  25.291 +by (cases_tac "ys" 1);
  25.292  by (Auto_tac);
  25.293  qed "list_all2_Cons1";
  25.294  
  25.295  Goalw [list_all2_def]
  25.296   "list_all2 P xs (y#ys) = (? z zs. xs = z#zs & P z y & list_all2 P zs ys)";
  25.297 -by (exhaust_tac "xs" 1);
  25.298 +by (cases_tac "xs" 1);
  25.299  by (Auto_tac);
  25.300  qed "list_all2_Cons2";
  25.301  
  25.302 @@ -1249,8 +1249,8 @@
  25.303  						all_conj_distrib])));
  25.304  by (Clarify_tac 1);
  25.305  (*Both lists must be non-empty*)
  25.306 -by (exhaust_tac "xs" 1);
  25.307 -by (exhaust_tac "ys" 2);
  25.308 +by (cases_tac "xs" 1);
  25.309 +by (cases_tac "ys" 2);
  25.310  by (ALLGOALS Clarify_tac);
  25.311  (*prenexing's needed, not miniscoping*)
  25.312  by (ALLGOALS (full_simp_tac (simpset() addsimps (all_simps RL [sym])  
  25.313 @@ -1412,7 +1412,7 @@
  25.314   by (rename_tac "a xys x xs' y ys'" 1);
  25.315   by (res_inst_tac [("x","a#xys")] exI 1);
  25.316   by (Simp_tac 1);
  25.317 -by (exhaust_tac "xys" 1);
  25.318 +by (cases_tac "xys" 1);
  25.319   by (ALLGOALS (asm_full_simp_tac (simpset())));
  25.320  by (Blast_tac 1);
  25.321  qed "lexn_conv";
  25.322 @@ -1452,7 +1452,7 @@
  25.323  by (rtac iffI 1);
  25.324   by (blast_tac (claset() addIs [Cons_eq_appendI]) 2);
  25.325  by (REPEAT(eresolve_tac [conjE, exE] 1));
  25.326 -by (exhaust_tac "xys" 1);
  25.327 +by (cases_tac "xys" 1);
  25.328  by (Asm_full_simp_tac 1);
  25.329  by (Asm_full_simp_tac 1);
  25.330  by (Blast_tac 1);
  25.331 @@ -1467,19 +1467,19 @@
  25.332  	   sum_eq_0_conv]);
  25.333  
  25.334  Goal "take n (x#xs) = (if n = #0 then [] else x # take (n-#1) xs)";
  25.335 -by (exhaust_tac "n" 1);
  25.336 +by (cases_tac "n" 1);
  25.337  by (ALLGOALS 
  25.338      (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1])));
  25.339  qed "take_Cons'";
  25.340  
  25.341  Goal "drop n (x#xs) = (if n = #0 then x#xs else drop (n-#1) xs)";
  25.342 -by (exhaust_tac "n" 1);
  25.343 +by (cases_tac "n" 1);
  25.344  by (ALLGOALS
  25.345      (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1])));
  25.346  qed "drop_Cons'";
  25.347  
  25.348  Goal "(x#xs)!n = (if n = #0 then x else xs!(n-#1))";
  25.349 -by (exhaust_tac "n" 1);
  25.350 +by (cases_tac "n" 1);
  25.351  by (ALLGOALS
  25.352      (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1])));
  25.353  qed "nth_Cons'";
    26.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML	Mon Mar 13 12:42:41 2000 +0100
    26.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML	Mon Mar 13 12:51:10 2000 +0100
    26.3 @@ -68,7 +68,7 @@
    26.4  be widen.induct 1;
    26.5  by(Auto_tac);
    26.6  by(rename_tac "R" 1);
    26.7 -by(exhaust_tac "R" 1);
    26.8 +by(cases_tac "R" 1);
    26.9  by(Auto_tac);
   26.10  val lemma = result();
   26.11  
   26.12 @@ -100,7 +100,7 @@
   26.13    ba 1;
   26.14   ba 1;
   26.15  by(rewtac wt_jvm_prog_def);
   26.16 -by (exhaust_tac "ls_com" 1);
   26.17 +by (cases_tac "ls_com" 1);
   26.18  by (ALLGOALS (fast_tac (claset() addIs [Load_correct,Store_correct,Bipush_correct,Aconst_null_correct])));
   26.19  qed "LS_correct";
   26.20  
   26.21 @@ -119,7 +119,7 @@
   26.22  by (asm_full_simp_tac (simpset() addsimps [conf_def]) 1);
   26.23  by (Clarify_tac 1);
   26.24  by (asm_full_simp_tac (simpset() addsimps [obj_ty_def]) 1);
   26.25 -by (exhaust_tac "v" 1);
   26.26 +by (cases_tac "v" 1);
   26.27  by (ALLGOALS (fast_tac  (claset() addIs [rtrancl_trans] addss (simpset() addsimps [widen.null]))));
   26.28  qed "Cast_conf2";
   26.29  
   26.30 @@ -149,7 +149,7 @@
   26.31    ba 1;
   26.32   ba 1;
   26.33  by(rewtac wt_jvm_prog_def);
   26.34 -by (exhaust_tac "ch_com" 1);
   26.35 +by (cases_tac "ch_com" 1);
   26.36  by (ALLGOALS (fast_tac (claset() addIs [Checkcast_correct])));
   26.37  qed "CH_correct";
   26.38  
   26.39 @@ -223,7 +223,7 @@
   26.40    ba 1;
   26.41   ba 1;
   26.42  by(rewtac wt_jvm_prog_def);
   26.43 -by (exhaust_tac "mo_com" 1);
   26.44 +by (cases_tac "mo_com" 1);
   26.45  by (ALLGOALS (fast_tac (claset() addIs [Getfield_correct,Putfield_correct])));
   26.46  qed "MO_correct";
   26.47  
   26.48 @@ -263,7 +263,7 @@
   26.49    ba 1;
   26.50   ba 1;
   26.51  by(rewtac wt_jvm_prog_def);
   26.52 -by (exhaust_tac "co_com" 1);
   26.53 +by (cases_tac "co_com" 1);
   26.54  by (ALLGOALS (fast_tac (claset() addIs [New_correct])));
   26.55  qed "CO_correct";
   26.56  
   26.57 @@ -282,7 +282,7 @@
   26.58  by(etac exE 1);
   26.59  by(asm_full_simp_tac (simpset() addsimps defs1) 1);
   26.60  by(Clarify_tac 1);
   26.61 -by(exhaust_tac "X\\<noteq>NT" 1); 
   26.62 +by(case_tac "X\\<noteq>NT" 1); 
   26.63   by (asm_full_simp_tac (simpset()addsimps[raise_xcpt_def]@defs1 
   26.64  	addsplits [option.split]) 1);
   26.65   by (Clarify_tac 1);
   26.66 @@ -360,7 +360,7 @@
   26.67  by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
   26.68    ba 1;
   26.69   ba 1;
   26.70 -by (exhaust_tac "mi_com" 1);
   26.71 +by (cases_tac "mi_com" 1);
   26.72  by (ALLGOALS (fast_tac (claset() addIs [Invoke_correct])));
   26.73  qed "MI_correct";
   26.74  
   26.75 @@ -401,7 +401,7 @@
   26.76  by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
   26.77    ba 1;
   26.78   ba 1;
   26.79 -by (exhaust_tac "mr" 1);
   26.80 +by (cases_tac "mr" 1);
   26.81  by (ALLGOALS (fast_tac (claset() addIs [Return_correct])));
   26.82  qed "MR_correct";
   26.83  
   26.84 @@ -442,7 +442,7 @@
   26.85    ba 1;
   26.86   ba 1;
   26.87  by(rewtac wt_jvm_prog_def);
   26.88 -by (exhaust_tac "br_com" 1);
   26.89 +by (cases_tac "br_com" 1);
   26.90  by (ALLGOALS (fast_tac (claset() addIs [Goto_correct,Ifiacmpeq_correct])));
   26.91  qed "BR_correct";
   26.92  
   26.93 @@ -521,7 +521,7 @@
   26.94    ba 1;
   26.95   ba 1;
   26.96  by(rewtac wt_jvm_prog_def);
   26.97 -by (exhaust_tac "os_com" 1);
   26.98 +by (cases_tac "os_com" 1);
   26.99  by (ALLGOALS (fast_tac (claset() addIs [Pop_correct,Dup_correct,Dup_x1_correct,Dup_x2_correct,Swap_correct])));
  26.100  qed "OS_correct";
  26.101  
  26.102 @@ -539,15 +539,15 @@
  26.103  \ \\<Longrightarrow> exec (G,state) = Some state' \\<longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
  26.104  by(split_all_tac 1);
  26.105  by(rename_tac "xp hp frs" 1);
  26.106 -by (exhaust_tac "xp" 1);
  26.107 - by (exhaust_tac "frs" 1);
  26.108 +by (cases_tac "xp" 1);
  26.109 + by (cases_tac "frs" 1);
  26.110    by (asm_full_simp_tac (simpset() addsimps exec.rules) 1);
  26.111   by(split_all_tac 1);
  26.112   by(hyp_subst_tac 1);
  26.113   by(forward_tac [correct_state_impl_Some_method] 1);
  26.114   by (force_tac (claset() addIs [LS_correct,CO_correct,MO_correct,CH_correct,MI_correct,MR_correct,OS_correct,
  26.115  	BR_correct], simpset() addsplits [split_if_asm,instr.split,instr.split_asm] addsimps exec.rules@[split_def]) 1);
  26.116 -by (exhaust_tac "frs" 1);
  26.117 +by (cases_tac "frs" 1);
  26.118   by (ALLGOALS(asm_full_simp_tac (simpset() addsimps exec.rules)));
  26.119  qed_spec_mp "BV_correct_1";
  26.120  
    27.1 --- a/src/HOL/MicroJava/BV/Convert.ML	Mon Mar 13 12:42:41 2000 +0100
    27.2 +++ b/src/HOL/MicroJava/BV/Convert.ML	Mon Mar 13 12:51:10 2000 +0100
    27.3 @@ -6,7 +6,7 @@
    27.4  
    27.5  
    27.6  Goalw[sup_ty_opt_def] "G \\<turnstile> t <=o t";
    27.7 -by (exhaust_tac "t" 1);
    27.8 +by (cases_tac "t" 1);
    27.9  by Auto_tac;
   27.10  qed "sup_ty_opt_refl";
   27.11  Addsimps [sup_ty_opt_refl];
   27.12 @@ -66,7 +66,7 @@
   27.13  by (induct_tac "a" 1);
   27.14   by (Simp_tac 1);
   27.15  by (Clarsimp_tac 1);
   27.16 -by (exhaust_tac "n" 1);
   27.17 +by (cases_tac "n" 1);
   27.18   by (Asm_full_simp_tac 1);
   27.19  by (eres_inst_tac [("x","nat")] allE 1);
   27.20  by (smp_tac 1 1);
   27.21 @@ -89,7 +89,7 @@
   27.22  by (induct_tac "a" 1);
   27.23   by (Clarsimp_tac 1);
   27.24  by (Clarify_tac 1);
   27.25 -by (exhaust_tac "b" 1);
   27.26 +by (cases_tac "b" 1);
   27.27   by (Clarsimp_tac 1);  
   27.28  by (Clarsimp_tac 1);
   27.29  qed_spec_mp "sup_loc_append";
   27.30 @@ -112,7 +112,7 @@
   27.31  by (Clarsimp_tac 1);
   27.32  by Safe_tac;
   27.33   by (clarsimp_tac (claset(), simpset() addsimps [sup_loc_append, sup_loc_length]) 2);
   27.34 -by (exhaust_tac "b" 1); 
   27.35 +by (cases_tac "b" 1); 
   27.36   bd sup_loc_length 1;
   27.37   by (Clarsimp_tac 1);
   27.38  by (clarsimp_tac (claset(), simpset() addsimps [sup_loc_append, sup_loc_length]) 1);
   27.39 @@ -129,7 +129,7 @@
   27.40  qed "sup_state_rev_fst";
   27.41  
   27.42  Goal "map x a = Y # YT \\<longrightarrow> map x (tl a) = YT \\<and> x (hd a) = Y \\<and> (\\<exists> y yt. a = y#yt)";
   27.43 -by (exhaust_tac "a" 1);
   27.44 +by (cases_tac "a" 1);
   27.45  by Auto_tac;
   27.46  qed_spec_mp "map_hd_tl";
   27.47  
   27.48 @@ -159,15 +159,15 @@
   27.49  
   27.50  Goalw[sup_ty_opt_def] 
   27.51  "\\<lbrakk>G \\<turnstile> a <=o b; G \\<turnstile> b <=o c\\<rbrakk> \\<Longrightarrow> G \\<turnstile> a <=o c";
   27.52 -by (exhaust_tac "c" 1);
   27.53 +by (cases_tac "c" 1);
   27.54   by (Clarsimp_tac 1);
   27.55  by (Clarsimp_tac 1);
   27.56 -by (exhaust_tac "a" 1);
   27.57 +by (cases_tac "a" 1);
   27.58   by (Clarsimp_tac 1);
   27.59 - by (exhaust_tac "b" 1);
   27.60 + by (cases_tac "b" 1);
   27.61    by (Clarsimp_tac 1);
   27.62   by (Clarsimp_tac 1);
   27.63 -by (exhaust_tac "b" 1);
   27.64 +by (cases_tac "b" 1);
   27.65   by (Clarsimp_tac 1);
   27.66  by (Clarsimp_tac 1);
   27.67  be widen_trans 1;
   27.68 @@ -190,7 +190,7 @@
   27.69  by (induct_tac "a" 1);
   27.70   by (Clarsimp_tac 1);
   27.71  by (Clarsimp_tac 1);
   27.72 -by (exhaust_tac "b=[]" 1);
   27.73 +by (case_tac "b=[]" 1);
   27.74   by (Clarsimp_tac 1);
   27.75  by (Clarsimp_tac 1);
   27.76  by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
   27.77 @@ -230,7 +230,7 @@
   27.78  qed "sup_state_trans";
   27.79  
   27.80  Goalw[sup_ty_opt_def] "G \\<turnstile> a <=o Some b \\<Longrightarrow> \\<exists> x. a = Some x";
   27.81 -by (exhaust_tac "a" 1);
   27.82 +by (cases_tac "a" 1);
   27.83   by Auto_tac;
   27.84  qed "sup_ty_opt_some";
   27.85  
   27.86 @@ -240,7 +240,7 @@
   27.87  by (induct_tac "x" 1);
   27.88   by (Simp_tac 1);
   27.89  by (clarsimp_tac ((claset(), simpset()) addIffs [sup_loc_Cons2]) 1);
   27.90 -by (exhaust_tac "n" 1);
   27.91 +by (cases_tac "n" 1);
   27.92   by (clarsimp_tac (claset(), simpset() addsimps [list_all2_Cons1]) 1);
   27.93  by (clarsimp_tac (claset(), simpset() addsimps [list_all2_Cons1]) 1);
   27.94  qed_spec_mp "sup_loc_update";
    28.1 --- a/src/HOL/MicroJava/BV/Correct.ML	Mon Mar 13 12:42:41 2000 +0100
    28.2 +++ b/src/HOL/MicroJava/BV/Correct.ML	Mon Mar 13 12:51:10 2000 +0100
    28.3 @@ -40,7 +40,7 @@
    28.4  Goal
    28.5  "\\<lbrakk> wf_prog wt G \\<rbrakk> \
    28.6  \\\<Longrightarrow> approx_val G hp v (Some T) \\<longrightarrow> G\\<turnstile> T\\<preceq>T' \\<longrightarrow> approx_val G hp v (Some T')";
    28.7 -by (exhaust_tac "T" 1);
    28.8 +by (cases_tac "T" 1);
    28.9   by (Asm_simp_tac 1);
   28.10  by (fast_tac (claset() addIs [conf_widen] addss (simpset()addsimps[approx_val_def])) 1);
   28.11  qed_spec_mp "approx_val_imp_approx_val_assConvertible";
   28.12 @@ -56,7 +56,7 @@
   28.13  Goal
   28.14  "\\<lbrakk> hp a = Some obj' ; G,hp\\<turnstile> v\\<Colon>\\<preceq>T ; obj_ty obj = obj_ty obj' \\<rbrakk> \
   28.15  \\\<Longrightarrow>G,(hp(a\\<mapsto>obj))\\<turnstile> v\\<Colon>\\<preceq>T";
   28.16 -by (exhaust_tac "v" 1);
   28.17 +by (cases_tac "v" 1);
   28.18  by (auto_tac (claset() , simpset() addsimps [obj_ty_def,conf_def] addsplits [option.split]));
   28.19  qed_spec_mp "approx_val_imp_approx_val_heap_update";
   28.20  
   28.21 @@ -97,7 +97,7 @@
   28.22  
   28.23  Goalw [approx_loc_def,list_all2_def]
   28.24  "\\<forall> lvars. approx_loc G hp lvars lt \\<longrightarrow>  hp \\<le>| hp' \\<longrightarrow> approx_loc G hp' lvars lt";
   28.25 -by (exhaust_tac "lt" 1);
   28.26 +by (cases_tac "lt" 1);
   28.27   by (Asm_simp_tac 1);
   28.28  by (force_tac (claset() addIs [approx_val_imp_approx_val_sup_heap],
   28.29  	       simpset() addsimps [neq_Nil_conv]) 1);
    29.1 --- a/src/HOL/MicroJava/BV/LBVComplete.ML	Mon Mar 13 12:42:41 2000 +0100
    29.2 +++ b/src/HOL/MicroJava/BV/LBVComplete.ML	Mon Mar 13 12:51:10 2000 +0100
    29.3 @@ -7,14 +7,14 @@
    29.4  by (induct_tac "a" 1);
    29.5   by (Clarsimp_tac 1);
    29.6  by (Clarsimp_tac 1);
    29.7 -by (exhaust_tac "P n" 1);
    29.8 +by (case_tac "P n" 1);
    29.9   by (Clarsimp_tac 1);
   29.10 - by (exhaust_tac "na" 1);
   29.11 + by (cases_tac "na" 1);
   29.12    by (Clarsimp_tac 1);
   29.13   by (clarsimp_tac (claset(), simpset() addsimps [length_option_filter_n]) 1);
   29.14   by (Force_tac 1);
   29.15  by (Clarsimp_tac 1);
   29.16 -by (exhaust_tac "na" 1);
   29.17 +by (cases_tac "na" 1);
   29.18   by (Clarsimp_tac 1);
   29.19  by (force_tac (claset(), simpset() addsimps [length_option_filter_n]) 1);
   29.20  qed_spec_mp "is_approx_option_filter_n";
   29.21 @@ -28,7 +28,7 @@
   29.22  by (induct_tac "l" 1);
   29.23   by (Simp_tac 1);
   29.24  by (Clarify_tac 1);
   29.25 -by (exhaust_tac "n" 1);
   29.26 +by (cases_tac "n" 1);
   29.27   by (Clarsimp_tac 1);
   29.28  by (Clarsimp_tac 1);
   29.29  qed_spec_mp "option_filter_n_Some";
   29.30 @@ -90,7 +90,7 @@
   29.31  by (induct_tac "x" 1);
   29.32   by (Simp_tac 1);
   29.33  by (Clarsimp_tac 1);
   29.34 -by (exhaust_tac "n" 1);
   29.35 +by (cases_tac "n" 1);
   29.36   by (Clarsimp_tac 1);
   29.37  by (Clarsimp_tac 1);
   29.38  by (smp_tac 1 1);
   29.39 @@ -114,13 +114,13 @@
   29.40  
   29.41  
   29.42  Goal "G \\<turnstile> b \\<preceq> NT \\<Longrightarrow> b = NT";
   29.43 -by (exhaust_tac "b" 1);
   29.44 - by (exhaust_tac "ref_ty" 2);
   29.45 +by (cases_tac "b" 1);
   29.46 + by (cases_tac "ref_ty" 2);
   29.47  by Auto_tac;
   29.48  qed "widen_NT";
   29.49  
   29.50  Goal "G \\<turnstile> b \\<preceq> Class C \\<Longrightarrow> \\<exists>r. b = RefT r";
   29.51 -by (exhaust_tac "b" 1);
   29.52 +by (cases_tac "b" 1);
   29.53  by Auto_tac;
   29.54  qed "widen_Class";
   29.55  
   29.56 @@ -129,7 +129,7 @@
   29.57  by (induct_tac "a" 1);
   29.58   by (Clarsimp_tac 1);
   29.59  by (Clarsimp_tac 1);
   29.60 -by (exhaust_tac "b" 1);
   29.61 +by (cases_tac "b" 1);
   29.62   by (Clarsimp_tac 1);
   29.63  by (Clarsimp_tac 1);
   29.64  qed_spec_mp "all_widen_is_sup_loc";
   29.65 @@ -139,7 +139,7 @@
   29.66  \      G \\<turnstile> (x, y) <=s s1; wtl_inst i G rT s1 s1' cert mpc pc\\<rbrakk> \
   29.67  \       \\<Longrightarrow> \\<exists>s2'. wtl_inst i G rT (x, y) s2' cert mpc pc \\<and> \
   29.68  \                ((G \\<turnstile> s2' <=s s1') \\<or> (\\<exists> s. cert ! (Suc pc) = Some s \\<and> (G \\<turnstile> s2' <=s s)))"; 
   29.69 -by (exhaust_tac "meth_inv" 1); 
   29.70 +by (cases_tac "meth_inv" 1); 
   29.71  by (Clarsimp_tac 1);
   29.72  by (cut_inst_tac [("x","x"),("n","length apTs")] rev_append_cons 1);
   29.73   by (asm_full_simp_tac (simpset() addsimps [sup_state_length_fst]) 1);
   29.74 @@ -150,7 +150,7 @@
   29.75  back();
   29.76  back();
   29.77  by (clarsimp_tac (claset(), simpset() addsimps [sup_state_rev_fst,sup_state_Cons1]) 1);
   29.78 -by (exhaust_tac "X = NT" 1);
   29.79 +by (case_tac "X = NT" 1);
   29.80   by (Clarsimp_tac 1);
   29.81   by (res_inst_tac [("x","a")] exI 1);
   29.82   by (res_inst_tac [("x","b")] exI 1);
   29.83 @@ -161,7 +161,7 @@
   29.84  by (strip_tac1 1);
   29.85  by (forward_tac [widen_Class] 1);
   29.86  by (Clarsimp_tac 1);
   29.87 -by (exhaust_tac "r" 1);
   29.88 +by (cases_tac "r" 1);
   29.89   by (Clarsimp_tac 1);
   29.90   by (res_inst_tac [("x","a")] exI 1);
   29.91   by (res_inst_tac [("x","b")] exI 1);
   29.92 @@ -198,7 +198,7 @@
   29.93  by (induct_tac "b" 1);
   29.94   by (Simp_tac 1);
   29.95  by (clarsimp_tac (claset(), simpset() addsimps [list_all2_Cons1]) 1);
   29.96 -by (exhaust_tac "n" 1);
   29.97 +by (cases_tac "n" 1);
   29.98   by (asm_full_simp_tac (simpset() addsimps [sup_ty_opt_some]) 1);
   29.99  by (smp_tac 1 1);
  29.100  by (Asm_full_simp_tac 1);
  29.101 @@ -224,7 +224,7 @@
  29.102  
  29.103  Goal "(G \\<turnstile> xb \\<preceq> PrimT p) = (xb = PrimT p)";
  29.104  by Safe_tac;
  29.105 -by (exhaust_tac "xb" 1);
  29.106 +by (cases_tac "xb" 1);
  29.107  by Auto_tac;
  29.108  bd widen_RefT 1;
  29.109  by Auto_tac;
  29.110 @@ -237,8 +237,8 @@
  29.111  \      (G \\<turnstile> s2' <=s s1' \\<or> (\\<exists>s. cert!(Suc pc) = Some s \\<and> G \\<turnstile> s2' <=s s))"; 
  29.112  by (cut_inst_tac [("z","s2")] surj_pair 1); 
  29.113  by (Clarify_tac 1); 
  29.114 -by (exhaust_tac "ins!pc" 1); 
  29.115 -       by (exhaust_tac "load_and_store" 1); 
  29.116 +by (cases_tac "ins!pc" 1); 
  29.117 +       by (cases_tac "load_and_store" 1); 
  29.118            by (Clarsimp_tac 1); 
  29.119            by (datac mono_load 2 1); 
  29.120            by (clarsimp_tac (claset(), simpset() addsimps [sup_state_length_snd]) 1);
  29.121 @@ -247,9 +247,9 @@
  29.122           by (Clarsimp_tac 1);
  29.123          by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons1]) 1); 
  29.124         by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons1]) 1); 
  29.125 -      by (exhaust_tac "create_object" 1); 
  29.126 +      by (cases_tac "create_object" 1); 
  29.127        by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons1]) 1); 
  29.128 -     by (exhaust_tac "manipulate_object" 1); 
  29.129 +     by (cases_tac "manipulate_object" 1); 
  29.130        by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
  29.131        be widen_trans 1; 
  29.132        ba 1; 
  29.133 @@ -259,7 +259,7 @@
  29.134        ba 1; 
  29.135       be widen_trans 1; 
  29.136       ba 1; 
  29.137 -    by (exhaust_tac "check_object" 1); 
  29.138 +    by (cases_tac "check_object" 1); 
  29.139      by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
  29.140      be widen_RefT2 1; 
  29.141      br method_inv_pseudo_mono 1;
  29.142 @@ -270,7 +270,7 @@
  29.143        ba 1;
  29.144       ba 1;
  29.145      ba 1;   
  29.146 -   by (exhaust_tac "meth_ret" 1);
  29.147 +   by (cases_tac "meth_ret" 1);
  29.148     by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
  29.149     br conjI 1;
  29.150      be widen_trans 1;
  29.151 @@ -278,13 +278,13 @@
  29.152     by (cut_inst_tac [("z","s1'")] surj_pair 1);
  29.153     by (strip_tac1 1);
  29.154     by (Clarsimp_tac 1);
  29.155 -  by (exhaust_tac "op_stack" 1);
  29.156 +  by (cases_tac "op_stack" 1);
  29.157       by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
  29.158      by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
  29.159     by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
  29.160    by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
  29.161   by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
  29.162 -by (exhaust_tac "branch" 1);
  29.163 +by (cases_tac "branch" 1);
  29.164   by (Clarsimp_tac 1);
  29.165   bd sup_state_trans 1;
  29.166    ba 1;
  29.167 @@ -298,10 +298,10 @@
  29.168    ba 2;
  29.169   ba 2;
  29.170  by (Clarsimp_tac 1);
  29.171 -by (exhaust_tac "xa" 1);
  29.172 +by (cases_tac "xa" 1);
  29.173   by (clarsimp_tac (claset(), simpset() addsimps [PrimT_PrimT]) 1);
  29.174  by (Clarsimp_tac 1);
  29.175 -by (exhaust_tac "xb" 1);
  29.176 +by (cases_tac "xb" 1);
  29.177  by Auto_tac;
  29.178  bd widen_RefT 1;
  29.179  by Auto_tac;
  29.180 @@ -310,15 +310,15 @@
  29.181  
  29.182  Goal "\\<lbrakk>wtl_inst i G rT s1 s1' cert (Suc pc) pc; G \\<turnstile> s2 <=s s1\\<rbrakk> \\<Longrightarrow> \
  29.183  \ \\<exists>s2'. wtl_inst i G rT s2 s2' cert (Suc pc) pc \\<and> (G \\<turnstile> s2' <=s s1')";
  29.184 -by (exhaust_tac "i" 1);
  29.185 -by (exhaust_tac "branch" 8);
  29.186 -by (exhaust_tac "op_stack" 7);
  29.187 -by (exhaust_tac "meth_ret" 6);
  29.188 -by (exhaust_tac "meth_inv" 5);
  29.189 -by (exhaust_tac "check_object" 4);
  29.190 -by (exhaust_tac "manipulate_object" 3);
  29.191 -by (exhaust_tac "create_object" 2);
  29.192 -by (exhaust_tac "load_and_store" 1);
  29.193 +by (cases_tac "i" 1);
  29.194 +by (cases_tac "branch" 8);
  29.195 +by (cases_tac "op_stack" 7);
  29.196 +by (cases_tac "meth_ret" 6);
  29.197 +by (cases_tac "meth_inv" 5);
  29.198 +by (cases_tac "check_object" 4);
  29.199 +by (cases_tac "manipulate_object" 3);
  29.200 +by (cases_tac "create_object" 2);
  29.201 +by (cases_tac "load_and_store" 1);
  29.202  by (TRYALL Asm_full_simp_tac);
  29.203   by (pair_tac "s1'" 1);
  29.204   by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1);
  29.205 @@ -335,7 +335,7 @@
  29.206  Goalw [wtl_inst_option_def] 
  29.207  "\\<lbrakk>wtl_inst_option i G rT s1 s1' cert mpc pc; Suc pc = mpc; G \\<turnstile> s2 <=s s1\\<rbrakk> \\<Longrightarrow> \
  29.208  \ \\<exists>s2'. wtl_inst_option i G rT s2 s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')";
  29.209 -by (exhaust_tac "cert!pc" 1);
  29.210 +by (cases_tac "cert!pc" 1);
  29.211   by (Clarsimp_tac 1);
  29.212   bd wtl_inst_last_mono 1;
  29.213    ba 1;
  29.214 @@ -355,18 +355,18 @@
  29.215  \     \\<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";  
  29.216  by (cut_inst_tac [("z","phi!pc")] surj_pair 1);
  29.217  by (strip_tac1 1);
  29.218 -by (exhaust_tac "ins!pc" 1);
  29.219 -by (exhaust_tac "op_stack" 7);
  29.220 -by (exhaust_tac "check_object" 4);
  29.221 -by (exhaust_tac "manipulate_object" 3);
  29.222 -by (exhaust_tac "create_object" 2);
  29.223 -by (exhaust_tac "load_and_store" 1);
  29.224 +by (cases_tac "ins!pc" 1);
  29.225 +by (cases_tac "op_stack" 7);
  29.226 +by (cases_tac "check_object" 4);
  29.227 +by (cases_tac "manipulate_object" 3);
  29.228 +by (cases_tac "create_object" 2);
  29.229 +by (cases_tac "load_and_store" 1);
  29.230                 by (TRYALL (Asm_full_simp_tac THEN_MAYBE' Force_tac));
  29.231 -  by (exhaust_tac "meth_inv" 1);
  29.232 +  by (cases_tac "meth_inv" 1);
  29.233    by (cut_inst_tac [("z","phi!(Suc pc)")] surj_pair 1);
  29.234    by (strip_tac1 1);
  29.235    by (Clarsimp_tac 1);
  29.236 -  by (exhaust_tac "X = NT" 1);
  29.237 +  by (case_tac "X = NT" 1);
  29.238     by (clarsimp_tac (claset(),simpset() addsimps [fits_def, contains_dead_def]) 1);
  29.239     by (smp_tac 1 1);
  29.240     by (Clarsimp_tac 1);
  29.241 @@ -378,12 +378,12 @@
  29.242    by (Asm_full_simp_tac 1);
  29.243    by (res_inst_tac [("x","apTs")] exI 1);
  29.244    by (clarsimp_tac (claset(),simpset() addsimps [fits_def, contains_dead_def]) 1);
  29.245 - by (exhaust_tac "meth_ret" 1);
  29.246 + by (cases_tac "meth_ret" 1);
  29.247   by (asm_full_simp_tac (simpset() addsimps [fits_def, contains_dead_def]) 1);
  29.248   by (cut_inst_tac [("z","phi!Suc pc")] surj_pair 1);
  29.249   by (strip_tac1 1);
  29.250   by (Clarsimp_tac 1);
  29.251 -by (exhaust_tac "branch" 1);
  29.252 +by (cases_tac "branch" 1);
  29.253   by (asm_full_simp_tac (simpset() addsimps [fits_def, contains_dead_def, contains_targets_def]) 1);
  29.254   by (cut_inst_tac [("z","phi!Suc pc")] surj_pair 1);
  29.255   by (Force_tac 1);
  29.256 @@ -395,7 +395,7 @@
  29.257       "\\<lbrakk>fits ins cert phi; pc < length ins; wt_instr (ins!pc) G rT phi max_pc pc; \
  29.258  \      max_pc = length ins\\<rbrakk> \\<Longrightarrow> \ 
  29.259  \     \\<exists> s. wtl_inst_option (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";
  29.260 -by (exhaust_tac "cert!pc" 1);
  29.261 +by (cases_tac "cert!pc" 1);
  29.262   by (Clarsimp_tac 1);
  29.263   bd wt_instr_imp_wtl_inst 1;
  29.264      ba 1;
  29.265 @@ -417,14 +417,14 @@
  29.266  \     ins \\<noteq> []; G \\<turnstile> s <=s s0; \ 
  29.267  \     s \\<noteq> s0 \\<longrightarrow> cert ! pc = Some s0\\<rbrakk> \\<Longrightarrow> \ 
  29.268  \     wtl_inst_list ins G rT s s' cert max_pc pc";  
  29.269 -by (exhaust_tac "ins" 1); 
  29.270 +by (cases_tac "ins" 1); 
  29.271   by (Clarify_tac 1);
  29.272  by (Clarify_tac 1);
  29.273  by (Asm_full_simp_tac 1);
  29.274  by (Clarify_tac 1);
  29.275 -by (exhaust_tac "list = []" 1);
  29.276 +by (case_tac "list = []" 1);
  29.277   by (Asm_full_simp_tac 1);
  29.278 - by (exhaust_tac "s = s0" 1);
  29.279 + by (case_tac "s = s0" 1);
  29.280    by (Force_tac 1);
  29.281   by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
  29.282  by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
  29.283 @@ -434,7 +434,7 @@
  29.284  Goal "\\<lbrakk>wtl_inst_list ins G rT s0 s' cert max_pc pc; \ 
  29.285  \     ins \\<noteq> []; G \\<turnstile> s <=s s0; cert ! pc = Some s0\\<rbrakk> \\<Longrightarrow> \ 
  29.286  \     wtl_inst_list ins G rT s s' cert max_pc pc"; 
  29.287 -by (exhaust_tac "ins" 1); 
  29.288 +by (cases_tac "ins" 1); 
  29.289   by (Clarify_tac 1);
  29.290  by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
  29.291  qed "wtl_inst_list_cert";
  29.292 @@ -446,7 +446,7 @@
  29.293  \ G \\<turnstile> s2 <=s s1; i = ins!pc\\<rbrakk> \\<Longrightarrow> \
  29.294  \ \\<exists> s2'. wtl_inst_option (ins!pc) G rT s2 s2' cert mpc pc \\<and> \
  29.295  \        (G \\<turnstile> s2' <=s s1' \\<or> (\\<exists>s. cert!(Suc pc) = Some s \\<and> G \\<turnstile> s2' <=s s))";
  29.296 -by (exhaust_tac "cert!pc" 1);
  29.297 +by (cases_tac "cert!pc" 1);
  29.298   by (Asm_full_simp_tac 1);
  29.299   by (datac wtl_inst_pseudo_mono 4 1);
  29.300    by (Clarsimp_tac 1);
  29.301 @@ -495,7 +495,7 @@
  29.302   by (Simp_tac 1);
  29.303  by (asm_full_simp_tac (simpset() addsimps [nth_append]) 1);
  29.304  by (Clarify_tac 1);
  29.305 -by (exhaust_tac "list = []" 1);
  29.306 +by (case_tac "list = []" 1);
  29.307   by (Clarsimp_tac 1);
  29.308   bd wtl_option_last_mono 1;
  29.309     br refl 1;
  29.310 @@ -512,7 +512,7 @@
  29.311    ba 1;
  29.312   by (simp_tac (simpset() addsimps [append_cons_length_nth]) 1);
  29.313  by (clarsimp_tac (claset(), simpset() addsimps [append_cons_length_nth]) 1);
  29.314 -by (exhaust_tac "cert ! Suc (length l)" 1);
  29.315 +by (cases_tac "cert ! Suc (length l)" 1);
  29.316   by (Clarsimp_tac 1);
  29.317   by (dres_inst_tac [("a","(ac,bb)")] sup_state_trans 1);
  29.318    ba 1;
  29.319 @@ -529,7 +529,7 @@
  29.320  by (clarsimp_tac (claset(), simpset() addsimps [fits_def, is_approx_def]) 1);
  29.321  by (eres_inst_tac [("x","Suc (length l)")] allE 1);
  29.322  be impE 1;
  29.323 - by (exhaust_tac "length list" 1);
  29.324 + by (cases_tac "length list" 1);
  29.325    by (Clarsimp_tac 1);
  29.326   by (Clarsimp_tac 1);
  29.327  by (Clarsimp_tac 1);
    30.1 --- a/src/HOL/MicroJava/BV/LBVCorrect.ML	Mon Mar 13 12:42:41 2000 +0100
    30.2 +++ b/src/HOL/MicroJava/BV/LBVCorrect.ML	Mon Mar 13 12:51:10 2000 +0100
    30.3 @@ -25,11 +25,11 @@
    30.4  by (eres_inst_tac [("x","Suc pc")] allE 1);
    30.5  by (Asm_full_simp_tac 1);
    30.6  by (Clarify_tac 1);
    30.7 -by (exhaust_tac "cert ! pc" 1);
    30.8 +by (cases_tac "cert ! pc" 1);
    30.9   by (res_inst_tac [("x","phi[pc:=(aa, b)]")] exI 1);
   30.10   by (asm_full_simp_tac (simpset() addsimps [fits_partial_def]) 1);
   30.11   by (Clarify_tac 1);
   30.12 - by (exhaust_tac "ac" 1);
   30.13 + by (cases_tac "ac" 1);
   30.14    by (Asm_full_simp_tac 1);
   30.15   by (Asm_full_simp_tac 1);
   30.16   by (Clarify_tac 1);
   30.17 @@ -46,7 +46,7 @@
   30.18  by (res_inst_tac [("x","phi[pc:=ac]")] exI 1);
   30.19  by (asm_full_simp_tac (simpset() addsimps [fits_partial_def]) 1);
   30.20  by (Clarify_tac 1);
   30.21 -by (exhaust_tac "ad" 1);
   30.22 +by (cases_tac "ad" 1);
   30.23   by (Asm_full_simp_tac 1);
   30.24  by (Asm_full_simp_tac 1);
   30.25  by (Clarify_tac 1);
   30.26 @@ -94,13 +94,13 @@
   30.27  by (forward_tac [wtl_append] 1);
   30.28    ba 1;
   30.29   ba 1;
   30.30 -by (exhaust_tac "b=[]" 1);
   30.31 +by (case_tac "b=[]" 1);
   30.32   by (Asm_full_simp_tac 1);
   30.33  by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
   30.34  by (Clarify_tac 1);
   30.35  by (Asm_full_simp_tac 1);
   30.36  by (Clarify_tac 1);
   30.37 -by (exhaust_tac "cert!(Suc (length a))" 1);
   30.38 +by (cases_tac "cert!(Suc (length a))" 1);
   30.39   by (asm_full_simp_tac (simpset() addsimps [fits_def, fits_partial_def]) 1);
   30.40   by (eres_inst_tac [("x","a@[i]")] allE 1);
   30.41   by (eres_inst_tac [("x","ys")] allE 1);
   30.42 @@ -161,46 +161,46 @@
   30.43  by (TRYALL atac);
   30.44  by (forward_tac [fits_lemma1] 1);
   30.45   ba 1;
   30.46 -by (exhaust_tac "cert!(length i1)" 1);
   30.47 +by (cases_tac "cert!(length i1)" 1);
   30.48   by (forward_tac [fits_lemma2] 1);
   30.49       by (TRYALL atac);
   30.50 - by (exhaust_tac "i" 1);
   30.51 -        by (exhaust_tac "check_object" 4);
   30.52 -        by (exhaust_tac "manipulate_object" 3);
   30.53 -         by (exhaust_tac "create_object" 2);
   30.54 -         by (exhaust_tac "load_and_store" 1);
   30.55 + by (cases_tac "i" 1);
   30.56 +        by (cases_tac "check_object" 4);
   30.57 +        by (cases_tac "manipulate_object" 3);
   30.58 +         by (cases_tac "create_object" 2);
   30.59 +         by (cases_tac "load_and_store" 1);
   30.60              by (GOALS (force_tac (claset(), 
   30.61                  simpset() addsimps [wt_instr_def,wtl_inst_option_def])) 1 8);
   30.62 -    by (exhaust_tac "meth_inv" 1);
   30.63 +    by (cases_tac "meth_inv" 1);
   30.64      by (thin_tac "\\<forall>pc t.\
   30.65  \                 pc < length (i1 @ i # i2) \\<longrightarrow> \
   30.66  \                 cert ! pc = Some t \\<longrightarrow> phi ! pc = t" 1);
   30.67      by (pair_tac "s1" 1);
   30.68      by (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 1);    
   30.69      by (Force_tac 1);
   30.70 -   by (exhaust_tac "meth_ret" 1);
   30.71 +   by (cases_tac "meth_ret" 1);
   30.72     by (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 1);
   30.73 -  by (exhaust_tac "branch" 2);
   30.74 -   by (exhaust_tac "op_stack" 1);
   30.75 +  by (cases_tac "branch" 2);
   30.76 +   by (cases_tac "op_stack" 1);
   30.77         by (GOALS (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 
   30.78                    THEN_MAYBE' Force_tac) 1 7);
   30.79  by (forw_inst_tac [("x","length i1")] spec 1);
   30.80  by (eres_inst_tac [("x","a")] allE 1);
   30.81 -by (exhaust_tac "i" 1);
   30.82 -       by (exhaust_tac "check_object" 4);
   30.83 -       by (exhaust_tac "manipulate_object" 3);
   30.84 -        by (exhaust_tac "create_object" 2);
   30.85 -        by (exhaust_tac "load_and_store" 1);
   30.86 +by (cases_tac "i" 1);
   30.87 +       by (cases_tac "check_object" 4);
   30.88 +       by (cases_tac "manipulate_object" 3);
   30.89 +        by (cases_tac "create_object" 2);
   30.90 +        by (cases_tac "load_and_store" 1);
   30.91             by (GOALS (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 
   30.92                        THEN' Force_tac) 1 8);
   30.93 -   by (exhaust_tac "meth_inv" 1);
   30.94 +   by (cases_tac "meth_inv" 1);
   30.95     by (thin_tac "\\<forall>pc t.\
   30.96  \                pc < length (i1 @ i # i2) \\<longrightarrow> \
   30.97  \                cert ! pc = Some t \\<longrightarrow> phi ! pc = t" 1);
   30.98     by (force_tac (claset(), simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 1);
   30.99 -  by (exhaust_tac "branch" 3);
  30.100 -   by (exhaust_tac "op_stack" 2);
  30.101 -       by (exhaust_tac "meth_ret" 1);
  30.102 +  by (cases_tac "branch" 3);
  30.103 +   by (cases_tac "op_stack" 2);
  30.104 +       by (cases_tac "meth_ret" 1);
  30.105         by (GOALS (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 
  30.106                    THEN_MAYBE' Force_tac) 1 8);
  30.107  qed "wtl_lemma";
  30.108 @@ -242,7 +242,7 @@
  30.109  by (Asm_full_simp_tac 1);
  30.110  be impE 1;
  30.111  by (Force_tac 1);
  30.112 -by (exhaust_tac "cert ! 0" 1);
  30.113 +by (cases_tac "cert ! 0" 1);
  30.114  by (auto_tac (claset(), simpset() addsimps [wtl_inst_option_def]));
  30.115  qed "fits_first";
  30.116  
    31.1 --- a/src/HOL/MicroJava/BV/LBVSpec.ML	Mon Mar 13 12:42:41 2000 +0100
    31.2 +++ b/src/HOL/MicroJava/BV/LBVSpec.ML	Mon Mar 13 12:51:10 2000 +0100
    31.3 @@ -11,15 +11,15 @@
    31.4  
    31.5  Goal "\\<lbrakk>wtl_inst i G rT s0 s1 cert max_pc pc; \
    31.6  \      wtl_inst i G rT s0 s1' cert max_pc pc\\<rbrakk> \\<Longrightarrow> s1 = s1'";
    31.7 -by (exhaust_tac "i" 1);
    31.8 -by (exhaust_tac "branch" 8);
    31.9 -by (exhaust_tac "op_stack" 7);
   31.10 -by (exhaust_tac "meth_ret" 6);
   31.11 -by (exhaust_tac "meth_inv" 5);
   31.12 -by (exhaust_tac "check_object" 4);
   31.13 -by (exhaust_tac "manipulate_object" 3);
   31.14 -by (exhaust_tac "create_object" 2);
   31.15 -by (exhaust_tac "load_and_store" 1);
   31.16 +by (cases_tac "i" 1);
   31.17 +by (cases_tac "branch" 8);
   31.18 +by (cases_tac "op_stack" 7);
   31.19 +by (cases_tac "meth_ret" 6);
   31.20 +by (cases_tac "meth_inv" 5);
   31.21 +by (cases_tac "check_object" 4);
   31.22 +by (cases_tac "manipulate_object" 3);
   31.23 +by (cases_tac "create_object" 2);
   31.24 +by (cases_tac "load_and_store" 1);
   31.25  by Auto_tac;
   31.26  by (ALLGOALS (dtac rev_eq));
   31.27  by (TRYALL atac);
   31.28 @@ -29,7 +29,7 @@
   31.29  
   31.30  Goal "\\<lbrakk>wtl_inst_option i G rT s0 s1 cert max_pc pc; \
   31.31  \      wtl_inst_option i G rT s0 s1' cert max_pc pc\\<rbrakk> \\<Longrightarrow> s1 = s1'";
   31.32 -by (exhaust_tac "cert!pc" 1);
   31.33 +by (cases_tac "cert!pc" 1);
   31.34  by (auto_tac (claset(), simpset() addsimps [wtl_inst_unique, wtl_inst_option_def]));
   31.35  qed "wtl_inst_option_unique";
   31.36  
   31.37 @@ -49,12 +49,12 @@
   31.38  \                  wtl_inst_list b G rT s1 s' cert mpc (pc+length a))";
   31.39  by(induct_tac "is" 1);
   31.40   by Auto_tac;
   31.41 -by (exhaust_tac "pc'" 1);
   31.42 +by (cases_tac "pc'" 1);
   31.43   by (dres_inst_tac [("x","pc'")] spec 1);
   31.44   by (smp_tac 3 1);
   31.45   by (res_inst_tac [("x","[]")] exI 1);
   31.46   by (Asm_full_simp_tac 1);
   31.47 - by (exhaust_tac "cert!pc" 1);
   31.48 + by (cases_tac "cert!pc" 1);
   31.49    by (Force_tac 1);
   31.50   by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
   31.51  by (dres_inst_tac [("x","nat")] spec 1);
    32.1 --- a/src/HOL/MicroJava/J/JBasis.ML	Mon Mar 13 12:42:41 2000 +0100
    32.2 +++ b/src/HOL/MicroJava/J/JBasis.ML	Mon Mar 13 12:51:10 2000 +0100
    32.3 @@ -83,7 +83,7 @@
    32.4  	eresolve_tac prems 1]);
    32.5  
    32.6  fun option_case_tac2 s i = EVERY [
    32.7 -	 exhaust_tac s i,
    32.8 +	 cases_tac s i,
    32.9  	 rotate_tac ~1 (i+1), asm_full_simp_tac HOL_basic_ss (i+1), 
   32.10  	 rotate_tac ~1  i   , asm_full_simp_tac HOL_basic_ss i];
   32.11  
    33.1 --- a/src/HOL/MicroJava/J/JTypeSafe.ML	Mon Mar 13 12:42:41 2000 +0100
    33.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.ML	Mon Mar 13 12:51:10 2000 +0100
    33.3 @@ -284,7 +284,7 @@
    33.4  (* Level 45 *)
    33.5  
    33.6  (* 1 Call *)
    33.7 -by( exhaust_tac "x" 1);
    33.8 +by( cases_tac "x" 1);
    33.9  by(  Clarsimp_tac 2);
   33.10  by(  dtac exec_xcpt 2);
   33.11  by(  Asm_full_simp_tac 2);
    34.1 --- a/src/HOL/MicroJava/J/Type.ML	Mon Mar 13 12:42:41 2000 +0100
    34.2 +++ b/src/HOL/MicroJava/J/Type.ML	Mon Mar 13 12:51:10 2000 +0100
    34.3 @@ -5,6 +5,6 @@
    34.4  *)
    34.5  
    34.6  Goal "(\\<forall>pt. T \\<noteq> PrimT pt) = (\\<exists>t. T = RefT t)";
    34.7 -by(exhaust_tac "T" 1);
    34.8 +by(cases_tac "T" 1);
    34.9  by Auto_tac;
   34.10  qed "non_PrimT";
    35.1 --- a/src/HOL/Nat.ML	Mon Mar 13 12:42:41 2000 +0100
    35.2 +++ b/src/HOL/Nat.ML	Mon Mar 13 12:51:10 2000 +0100
    35.3 @@ -22,23 +22,23 @@
    35.4  val [nat_case_0, nat_case_Suc] = nat.cases;
    35.5  
    35.6  Goal "n ~= 0 ==> EX m. n = Suc m";
    35.7 -by (exhaust_tac "n" 1);
    35.8 +by (cases_tac "n" 1);
    35.9  by (REPEAT (Blast_tac 1));
   35.10  qed "not0_implies_Suc";
   35.11  
   35.12  Goal "m<n ==> n ~= 0";
   35.13 -by (exhaust_tac "n" 1);
   35.14 +by (cases_tac "n" 1);
   35.15  by (ALLGOALS Asm_full_simp_tac);
   35.16  qed "gr_implies_not0";
   35.17  
   35.18  Goal "(n ~= 0) = (0 < n)";
   35.19 -by (exhaust_tac "n" 1);
   35.20 +by (cases_tac "n" 1);
   35.21  by Auto_tac;
   35.22  qed "neq0_conv";
   35.23  AddIffs [neq0_conv];
   35.24  
   35.25  Goal "(0 ~= n) = (0 < n)";
   35.26 -by (exhaust_tac "n" 1);
   35.27 +by (cases_tac "n" 1);
   35.28  by Auto_tac;
   35.29  qed "zero_neq_conv";
   35.30  AddIffs [zero_neq_conv];
   35.31 @@ -64,7 +64,7 @@
   35.32  
   35.33  (*Useful in certain inductive arguments*)
   35.34  Goal "(m < Suc n) = (m=0 | (EX j. m = Suc j & j < n))";
   35.35 -by (exhaust_tac "m" 1);
   35.36 +by (cases_tac "m" 1);
   35.37  by Auto_tac;
   35.38  qed "less_Suc_eq_0_disj";
   35.39  
   35.40 @@ -74,11 +74,11 @@
   35.41  by (fold_goals_tac [Least_nat_def]);
   35.42  by (safe_tac (claset() addSEs [LeastI]));
   35.43  by (rename_tac "j" 1);
   35.44 -by (exhaust_tac "j" 1);
   35.45 +by (cases_tac "j" 1);
   35.46  by (Blast_tac 1);
   35.47  by (blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1);
   35.48  by (rename_tac "k n" 1);
   35.49 -by (exhaust_tac "k" 1);
   35.50 +by (cases_tac "k" 1);
   35.51  by (Blast_tac 1);
   35.52  by (hyp_subst_tac 1);
   35.53  by (rewtac Least_nat_def);
   35.54 @@ -90,8 +90,8 @@
   35.55  
   35.56  val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
   35.57  by (rtac less_induct 1);
   35.58 -by (exhaust_tac "n" 1);
   35.59 -by (exhaust_tac "nat" 2);
   35.60 +by (cases_tac "n" 1);
   35.61 +by (cases_tac "nat" 2);
   35.62  by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans])));
   35.63  qed "nat_induct2";
   35.64  
    36.1 --- a/src/HOL/Option.ML	Mon Mar 13 12:42:41 2000 +0100
    36.2 +++ b/src/HOL/Option.ML	Mon Mar 13 12:51:10 2000 +0100
    36.3 @@ -82,13 +82,13 @@
    36.4  
    36.5  
    36.6  Goal "x : o2s xo = (xo = Some x)";
    36.7 -by (exhaust_tac "xo" 1);
    36.8 +by (cases_tac "xo" 1);
    36.9  by Auto_tac;
   36.10  qed "elem_o2s";
   36.11  AddIffs [elem_o2s];
   36.12  
   36.13  Goal "(o2s xo = {}) = (xo = None)";
   36.14 -by (exhaust_tac "xo" 1);
   36.15 +by (cases_tac "xo" 1);
   36.16  by Auto_tac;
   36.17  qed "o2s_empty_eq";
   36.18  
    37.1 --- a/src/HOL/Power.ML	Mon Mar 13 12:42:41 2000 +0100
    37.2 +++ b/src/HOL/Power.ML	Mon Mar 13 12:51:10 2000 +0100
    37.3 @@ -48,7 +48,7 @@
    37.4  (*** Binomial Coefficients, following Andy Gordon and Florian Kammueller ***)
    37.5  
    37.6  Goal "(n choose 0) = 1";
    37.7 -by (exhaust_tac "n" 1);
    37.8 +by (cases_tac "n" 1);
    37.9  by (ALLGOALS Asm_simp_tac);
   37.10  qed "binomial_n_0";
   37.11  
   37.12 @@ -99,7 +99,7 @@
   37.13  by (induct_tac "n" 1);
   37.14  by (simp_tac (simpset() addsimps [binomial_0]) 1);
   37.15  by (Clarify_tac 1);
   37.16 -by (exhaust_tac "k" 1);
   37.17 +by (cases_tac "k" 1);
   37.18  by (auto_tac (claset(),
   37.19  	      simpset() addsimps [add_mult_distrib, add_mult_distrib2,
   37.20  				  le_Suc_eq, binomial_eq_0]));
    38.1 --- a/src/HOL/Real/RealPow.ML	Mon Mar 13 12:42:41 2000 +0100
    38.2 +++ b/src/HOL/Real/RealPow.ML	Mon Mar 13 12:51:10 2000 +0100
    38.3 @@ -234,7 +234,7 @@
    38.4  qed_spec_mp "realpow_Suc_le";
    38.5  
    38.6  Goal "0r <= 0r ^ n";
    38.7 -by (exhaust_tac "n" 1);
    38.8 +by (cases_tac "n" 1);
    38.9  by (Auto_tac);
   38.10  qed "realpow_zero_le";
   38.11  Addsimps [realpow_zero_le];
    39.1 --- a/src/HOL/RelPow.ML	Mon Mar 13 12:42:41 2000 +0100
    39.2 +++ b/src/HOL/RelPow.ML	Mon Mar 13 12:51:10 2000 +0100
    39.3 @@ -43,7 +43,7 @@
    39.4  \       !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P  \
    39.5  \    |] ==> P";
    39.6  by (cut_facts_tac [p1] 1);
    39.7 -by (exhaust_tac "n" 1);
    39.8 +by (cases_tac "n" 1);
    39.9  by (asm_full_simp_tac (simpset() addsimps [p2]) 1);
   39.10  by (Asm_full_simp_tac 1);
   39.11  by (etac compEpair 1);
   39.12 @@ -70,7 +70,7 @@
   39.13  \       !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P  \
   39.14  \    |] ==> P";
   39.15  by (cut_facts_tac [p1] 1);
   39.16 -by (exhaust_tac "n" 1);
   39.17 +by (cases_tac "n" 1);
   39.18  by (asm_full_simp_tac (simpset() addsimps [p2]) 1);
   39.19  by (Asm_full_simp_tac 1);
   39.20  by (etac compEpair 1);
    40.1 --- a/src/HOL/TLA/Inc/Inc.ML	Mon Mar 13 12:42:41 2000 +0100
    40.2 +++ b/src/HOL/TLA/Inc/Inc.ML	Mon Mar 13 12:51:10 2000 +0100
    40.3 @@ -165,7 +165,7 @@
    40.4    (fn _ => [auto_tac (Inc_css addsimps2 Init_defs
    40.5                                addSIs2 [(temp_use N2_leadsto_a) 
    40.6                                         RSN(2, (temp_use leadsto_init))]),
    40.7 -	    exhaust_tac "pc2 (st1 sigma)" 1,
    40.8 +	    cases_tac "pc2 (st1 sigma)" 1,
    40.9  	    Auto_tac
   40.10  	   ]);
   40.11  
   40.12 @@ -212,7 +212,7 @@
   40.13    (fn _ => [auto_tac (Inc_css addsimps2 Init_defs
   40.14                                addSIs2 [(temp_use N1_leadsto_b) 
   40.15                                         RSN(2, temp_use leadsto_init)]),
   40.16 -	    exhaust_tac "pc1 (st1 sigma)" 1,
   40.17 +	    cases_tac "pc1 (st1 sigma)" 1,
   40.18  	    Auto_tac
   40.19  	   ]);
   40.20  
    41.1 --- a/src/HOL/TLA/Memory/Memory.ML	Mon Mar 13 12:42:41 2000 +0100
    41.2 +++ b/src/HOL/TLA/Memory/Memory.ML	Mon Mar 13 12:51:10 2000 +0100
    41.3 @@ -123,7 +123,7 @@
    41.4  \        --> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))" (K [
    41.5  	     auto_tac (mem_css addsimps2 [enabled_disj]
    41.6  		                  addSIs2 [RWRNext_enabled]),
    41.7 -             exhaust_tac "arg(ch w p)" 1,
    41.8 +             cases_tac "arg(ch w p)" 1,
    41.9   	      action_simp_tac (simpset()addsimps[Read_def,enabled_ex])
   41.10  	                      [ReadInner_enabled,exI] [] 1,
   41.11                force_tac (mem_css addDs2 [base_pair]) 1,
    42.1 --- a/src/HOL/UNITY/GenPrefix.ML	Mon Mar 13 12:42:41 2000 +0100
    42.2 +++ b/src/HOL/UNITY/GenPrefix.ML	Mon Mar 13 12:51:10 2000 +0100
    42.3 @@ -129,7 +129,7 @@
    42.4  
    42.5  Goal "((xs, y#ys) : genPrefix r) = \
    42.6  \     (xs=[] | (EX z zs. xs=z#zs & (z,y) : r & (zs,ys) : genPrefix r))";
    42.7 -by (exhaust_tac "xs" 1);
    42.8 +by (cases_tac "xs" 1);
    42.9  by Auto_tac;
   42.10  qed "genPrefix_Cons";
   42.11  
   42.12 @@ -183,7 +183,7 @@
   42.13  \               --> (xs, ys) : genPrefix r --> (xs ! i, ys ! i) : r";
   42.14  by (induct_tac "xs" 1);
   42.15  by Auto_tac;
   42.16 -by (exhaust_tac "i" 1);
   42.17 +by (cases_tac "i" 1);
   42.18  by Auto_tac;
   42.19  qed_spec_mp "genPrefix_imp_nth";
   42.20  
   42.21 @@ -194,7 +194,7 @@
   42.22  by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq_0_disj, 
   42.23  						all_conj_distrib])));
   42.24  by (Clarify_tac 1);
   42.25 -by (exhaust_tac "ys" 1);
   42.26 +by (cases_tac "ys" 1);
   42.27  by (ALLGOALS Force_tac);
   42.28  qed_spec_mp "nth_imp_genPrefix";
   42.29  
    43.1 --- a/src/HOL/UNITY/Lift_prog.ML	Mon Mar 13 12:42:41 2000 +0100
    43.2 +++ b/src/HOL/UNITY/Lift_prog.ML	Mon Mar 13 12:51:10 2000 +0100
    43.3 @@ -16,7 +16,7 @@
    43.4  Goal "(insert_map i x (delete_map i g)) = g(i:=x)";
    43.5  by (rtac ext 1);
    43.6  by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
    43.7 -by (exhaust_tac "d" 1);
    43.8 +by (cases_tac "d" 1);
    43.9  by (ALLGOALS Asm_simp_tac);
   43.10  qed "insert_map_delete_map_eq";
   43.11  
    44.1 --- a/src/HOL/UNITY/TimerArray.ML	Mon Mar 13 12:42:41 2000 +0100
    44.2 +++ b/src/HOL/UNITY/TimerArray.ML	Mon Mar 13 12:51:10 2000 +0100
    44.3 @@ -15,7 +15,7 @@
    44.4  Goal "Timer : UNIV leadsTo {s. count s = 0}";
    44.5  by (res_inst_tac [("f", "count")] lessThan_induct 1);
    44.6  by (Simp_tac 1);
    44.7 -by (exhaust_tac "m" 1);
    44.8 +by (cases_tac "m" 1);
    44.9  by (force_tac (claset() addSIs [subset_imp_leadsTo], simpset()) 1);
   44.10  by (ensures_tac "decr" 1);
   44.11  qed "Timer_leadsTo_zero";
   44.12 @@ -36,7 +36,7 @@
   44.13  by (constrains_tac 2);
   44.14  (*Progress property for the array of Timers*)
   44.15  by (res_inst_tac [("f", "sub i o fst")] lessThan_induct 1);
   44.16 -by (exhaust_tac "m" 1);
   44.17 +by (cases_tac "m" 1);
   44.18  (*Annoying need to massage the conditions to have the form (... Times UNIV)*)
   44.19  by (auto_tac (claset() addIs [subset_imp_leadsTo], 
   44.20  	      simpset() addsimps [insert_absorb, lessThan_Suc RS sym,
    45.1 --- a/src/HOL/UNITY/Token.ML	Mon Mar 13 12:42:41 2000 +0100
    45.2 +++ b/src/HOL/UNITY/Token.ML	Mon Mar 13 12:51:10 2000 +0100
    45.3 @@ -16,7 +16,7 @@
    45.4  
    45.5  Goalw Token_defs "(s ~: E i) = (s : H i | s : T i)";
    45.6  by (Simp_tac 1);
    45.7 -by (exhaust_tac "proc s i" 1);
    45.8 +by (cases_tac "proc s i" 1);
    45.9  by Auto_tac;
   45.10  qed "not_E_eq";
   45.11  
    46.1 --- a/src/HOL/ex/BinEx.ML	Mon Mar 13 12:42:41 2000 +0100
    46.2 +++ b/src/HOL/ex/BinEx.ML	Mon Mar 13 12:51:10 2000 +0100
    46.3 @@ -323,13 +323,13 @@
    46.4  
    46.5  Goal "w: normal ==> bin_succ w : normal";
    46.6  by (etac normal.induct 1);
    46.7 -by (exhaust_tac "w" 4);
    46.8 +by (cases_tac "w" 4);
    46.9  by (auto_tac (claset(), simpset() addsimps [NCons_True, bin_succ_BIT]));
   46.10  qed "bin_succ_normal";
   46.11  
   46.12  Goal "w: normal ==> bin_pred w : normal";
   46.13  by (etac normal.induct 1);
   46.14 -by (exhaust_tac "w" 3);
   46.15 +by (cases_tac "w" 3);
   46.16  by (auto_tac (claset(), simpset() addsimps [NCons_False, bin_pred_BIT]));
   46.17  qed "bin_pred_normal";
   46.18  
    47.1 --- a/src/HOL/ex/Factorization.ML	Mon Mar 13 12:42:41 2000 +0100
    47.2 +++ b/src/HOL/ex/Factorization.ML	Mon Mar 13 12:51:10 2000 +0100
    47.3 @@ -10,12 +10,12 @@
    47.4  (* --- Arithmetic --- *)
    47.5  
    47.6  Goal "[| m ~= m*k; m ~= 1 |] ==> 1<m";
    47.7 -by (exhaust_tac "m" 1);
    47.8 +by (cases_tac "m" 1);
    47.9  by Auto_tac;
   47.10  qed "one_less_m";
   47.11  
   47.12  Goal "[| m ~= m*k; 1<m*k |] ==> 1<k";
   47.13 -by (exhaust_tac "k" 1);
   47.14 +by (cases_tac "k" 1);
   47.15  by Auto_tac;
   47.16  qed "one_less_k";
   47.17  
   47.18 @@ -24,7 +24,7 @@
   47.19  qed "mult_left_cancel";
   47.20  
   47.21  Goal "[| 0<m; m*n = m |] ==> n=1";
   47.22 -by (exhaust_tac "n" 1);
   47.23 +by (cases_tac "n" 1);
   47.24  by Auto_tac;
   47.25  qed "mn_eq_m_one";
   47.26  
   47.27 @@ -55,7 +55,7 @@
   47.28  
   47.29  Goalw [prime_def,dvd_def] "p:prime ==> ~(p dvd 1)";
   47.30  by Auto_tac;
   47.31 -by (exhaust_tac "k" 1);
   47.32 +by (cases_tac "k" 1);
   47.33  by Auto_tac;
   47.34  qed "prime_nd_one";
   47.35  
   47.36 @@ -78,7 +78,7 @@
   47.37  qed "primes_eq";
   47.38  
   47.39  Goalw [primel_def,prime_def] "[| primel xs; prod xs = 1 |] ==> xs = []";
   47.40 -by (exhaust_tac "xs" 1);
   47.41 +by (cases_tac "xs" 1);
   47.42  by (ALLGOALS Asm_full_simp_tac);
   47.43  qed "primel_one_empty";
   47.44  
   47.45 @@ -105,7 +105,7 @@
   47.46  
   47.47  Goal "nondec xs --> nondec (oinsert x xs)";
   47.48  by (induct_tac "xs" 1);
   47.49 -by (exhaust_tac "list" 2);
   47.50 +by (cases_tac "list" 2);
   47.51  by (ALLGOALS (Asm_full_simp_tac));
   47.52  qed_spec_mp "nondec_oinsert";
   47.53  
   47.54 @@ -123,9 +123,9 @@
   47.55  by (induct_tac "xs" 1);
   47.56  by Safe_tac;
   47.57  by (ALLGOALS Asm_full_simp_tac);
   47.58 -by (exhaust_tac "list" 1);
   47.59 +by (cases_tac "list" 1);
   47.60  by (ALLGOALS Asm_full_simp_tac);
   47.61 -by (exhaust_tac "list" 1);
   47.62 +by (cases_tac "list" 1);
   47.63  by (Asm_full_simp_tac 1);
   47.64  by (res_inst_tac [("y","aa"),("ys","lista")] x_less_y_oinsert 1); 
   47.65  by (ALLGOALS Asm_full_simp_tac);
   47.66 @@ -269,7 +269,7 @@
   47.67  \     --> xs <~~> ys)";
   47.68  by (res_inst_tac [("n","n")] less_induct 1);
   47.69  by Safe_tac;
   47.70 -by (exhaust_tac "xs" 1);
   47.71 +by (cases_tac "xs" 1);
   47.72  by (force_tac (claset() addIs [primel_one_empty], simpset()) 1);
   47.73  by (rtac (perm_primel_ex RS exE) 1);
   47.74  by (ALLGOALS Asm_full_simp_tac);
    48.1 --- a/src/HOL/ex/Primrec.ML	Mon Mar 13 12:42:41 2000 +0100
    48.2 +++ b/src/HOL/ex/Primrec.ML	Mon Mar 13 12:51:10 2000 +0100
    48.3 @@ -185,7 +185,7 @@
    48.4  by (induct_tac "l" 1);
    48.5  by (ALLGOALS Asm_simp_tac);
    48.6  by (rtac allI 1);
    48.7 -by (exhaust_tac "i" 1);
    48.8 +by (cases_tac "i" 1);
    48.9  by (asm_simp_tac (simpset() addsimps [le_add1, le_imp_less_Suc]) 1);
   48.10  by (Asm_simp_tac 1);
   48.11  by (blast_tac (claset() addIs [less_le_trans] 
   48.12 @@ -223,7 +223,7 @@
   48.13   "[| ALL l. f l + list_add l < ack(kf, list_add l); \
   48.14  \    ALL l. g l + list_add l < ack(kg, list_add l)  \
   48.15  \ |] ==> PREC f g l + list_add l < ack(Suc(kf+kg), list_add l)";
   48.16 -by (exhaust_tac "l" 1);
   48.17 +by (cases_tac "l" 1);
   48.18  by (ALLGOALS Asm_simp_tac);
   48.19  by (blast_tac (claset() addIs [less_trans]) 1);
   48.20  by (etac ssubst 1);  (*get rid of the needless assumption*)
    49.1 --- a/src/HOL/ex/Puzzle.ML	Mon Mar 13 12:42:41 2000 +0100
    49.2 +++ b/src/HOL/ex/Puzzle.ML	Mon Mar 13 12:51:10 2000 +0100
    49.3 @@ -14,7 +14,7 @@
    49.4  by (res_inst_tac [("n","k")] less_induct 1);
    49.5  by (rtac allI 1);
    49.6  by (rename_tac "i" 1);
    49.7 -by (exhaust_tac "i" 1);
    49.8 +by (cases_tac "i" 1);
    49.9   by (Asm_simp_tac 1);
   49.10  by (blast_tac (claset() addSIs [Suc_leI] addIs [le_less_trans]) 1);
   49.11  val lemma = result() RS spec RS mp;