# HG changeset patch
# User nipkow
# Date 895505518 -7200
# Node ID e67949e15255163fe0957b66fdbe9412557d9911
# Parent  1694e2daef8f495fe205072c8b11a87a9ea68833
snoc_induct/exhaust -> rev_induct_exhaust.

diff -r 1694e2daef8f -r e67949e15255 src/HOL/Lex/Prefix.ML
--- a/src/HOL/Lex/Prefix.ML	Mon May 18 17:31:49 1998 +0200
+++ b/src/HOL/Lex/Prefix.ML	Mon May 18 17:31:58 1998 +0200
@@ -47,7 +47,7 @@
 br iffI 1;
  be exE 1;
  by(rename_tac "zs" 1);
- by(res_inst_tac [("xs","zs")] snoc_eq_cases 1);
+ by(res_inst_tac [("xs","zs")] rev_exhaust 1);
   by(Asm_full_simp_tac 1);
  by(hyp_subst_tac 1);
  by(asm_full_simp_tac (simpset() delsimps [append_assoc]
@@ -90,7 +90,7 @@
 qed "prefix_Cons";
 
 goal thy "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))";
-by(res_inst_tac [("xs","zs")] snoc_induct 1);
+by(res_inst_tac [("xs","zs")] rev_induct 1);
  by(Simp_tac 1);
  by(Blast_tac 1);
 by(asm_full_simp_tac (simpset() delsimps [append_assoc]
diff -r 1694e2daef8f -r e67949e15255 src/HOL/Lex/RegExp2NAe.ML
--- a/src/HOL/Lex/RegExp2NAe.ML	Mon May 18 17:31:49 1998 +0200
+++ b/src/HOL/Lex/RegExp2NAe.ML	Mon May 18 17:31:58 1998 +0200
@@ -541,7 +541,7 @@
 \ (? us v. w = concat us @ v & \
 \             (!u:set us. accepts A u) & \
 \             (? r. (start A,r) : steps A v & rr = True#r))";
-by(res_inst_tac [("xs","w")] snoc_induct 1);
+by(res_inst_tac [("xs","w")] rev_induct 1);
  by (Asm_full_simp_tac 1);
  by (Clarify_tac 1);
  by(res_inst_tac [("x","[]")] exI 1);
@@ -649,7 +649,7 @@
  by(asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
  by(Blast_tac 1);
 by (Clarify_tac 1);
-by(res_inst_tac [("xs","us")] snoc_exhaust 1);
+by(res_inst_tac [("xs","us")] rev_exhaust 1);
  by(Asm_simp_tac 1);
  by(Blast_tac 1);
 by (Clarify_tac 1);