src/HOL/Lex/RegExp2NA.ML

 Goal
  "(start(union L R), q) : steps (union L R) w = \
 \ ( (w = [] & q = start(union L R)) | \
 \   (w ~= [] & (? p.  q = True  # p & (start L,p) : steps L w | \
 \                     q = False # p & (start R,p) : steps R w)))";
-by (exhaust_tac "w" 1);
+by (cases_tac "w" 1);
  by (Asm_simp_tac 1);
  by (Blast_tac 1);
 by (Asm_simp_tac 1);
 by (Blast_tac 1);
 qed "steps_union";

  by (Clarify_tac 1);
  by (res_inst_tac [("x","u")] exI 1);
  by (Simp_tac 1);
  by (Blast_tac 1);
 by (Clarify_tac 1);
-by (exhaust_tac "v" 1);
+by (cases_tac "v" 1);
  by (Asm_full_simp_tac 1);
  by (Blast_tac 1);
 by (Asm_full_simp_tac 1);
 by (Blast_tac 1);
 qed "accepts_conc";

 AddIffs [step_plus_conv];
 
 Goal
  "[| (start A,q) : steps A u; u ~= []; fin A p |] \
 \ ==> (p,q) : steps (plus A) u";
-by (exhaust_tac "u" 1);
+by (cases_tac "u" 1);
  by (Blast_tac 1);
 by (Asm_full_simp_tac 1);
 by (blast_tac (claset() addIs [steps_plusI]) 1);
 qed "fin_steps_plusI";
 

 by (Clarify_tac 1);
 by (etac disjE 1);
  by (res_inst_tac [("x","us")] exI 1);
  by (Asm_simp_tac 1);
  by (Blast_tac 1);
-by (exhaust_tac "v" 1);
+by (cases_tac "v" 1);
  by (res_inst_tac [("x","us")] exI 1);
  by (Asm_full_simp_tac 1);
 by (res_inst_tac [("x","us@[v]")] exI 1);
 by (asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
 by (Blast_tac 1);