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);