src/HOL/Lex/RegExp2NA.ML
changeset 8423 3c19160b6432
parent 7958 f531589c9fc1
child 8442 96023903c2df
     1.1 --- a/src/HOL/Lex/RegExp2NA.ML	Mon Mar 13 12:42:41 2000 +0100
     1.2 +++ b/src/HOL/Lex/RegExp2NA.ML	Mon Mar 13 12:51:10 2000 +0100
     1.3 @@ -112,7 +112,7 @@
     1.4  \ ( (w = [] & q = start(union L R)) | \
     1.5  \   (w ~= [] & (? p.  q = True  # p & (start L,p) : steps L w | \
     1.6  \                     q = False # p & (start R,p) : steps R w)))";
     1.7 -by (exhaust_tac "w" 1);
     1.8 +by (cases_tac "w" 1);
     1.9   by (Asm_simp_tac 1);
    1.10   by (Blast_tac 1);
    1.11  by (Asm_simp_tac 1);
    1.12 @@ -273,7 +273,7 @@
    1.13   by (Simp_tac 1);
    1.14   by (Blast_tac 1);
    1.15  by (Clarify_tac 1);
    1.16 -by (exhaust_tac "v" 1);
    1.17 +by (cases_tac "v" 1);
    1.18   by (Asm_full_simp_tac 1);
    1.19   by (Blast_tac 1);
    1.20  by (Asm_full_simp_tac 1);
    1.21 @@ -336,7 +336,7 @@
    1.22  Goal
    1.23   "[| (start A,q) : steps A u; u ~= []; fin A p |] \
    1.24  \ ==> (p,q) : steps (plus A) u";
    1.25 -by (exhaust_tac "u" 1);
    1.26 +by (cases_tac "u" 1);
    1.27   by (Blast_tac 1);
    1.28  by (Asm_full_simp_tac 1);
    1.29  by (blast_tac (claset() addIs [steps_plusI]) 1);
    1.30 @@ -360,7 +360,7 @@
    1.31   by (res_inst_tac [("x","us")] exI 1);
    1.32   by (Asm_simp_tac 1);
    1.33   by (Blast_tac 1);
    1.34 -by (exhaust_tac "v" 1);
    1.35 +by (cases_tac "v" 1);
    1.36   by (res_inst_tac [("x","us")] exI 1);
    1.37   by (Asm_full_simp_tac 1);
    1.38  by (res_inst_tac [("x","us@[v]")] exI 1);