# HG changeset patch
# User nipkow
# Date 900758469 -7200
# Node ID e7457679e26df01e9b88769f419da3bf388466b7
# Parent  1ff6679144b90e3fca1ed3a6bb82a8856eb4f27c
Simplified last proof.

diff -r 1ff6679144b9 -r e7457679e26d src/HOL/Lex/MaxChop.ML
--- a/src/HOL/Lex/MaxChop.ML	Fri Jul 17 11:25:20 1998 +0200
+++ b/src/HOL/Lex/MaxChop.ML	Sat Jul 18 12:41:09 1998 +0200
@@ -80,26 +80,22 @@
  by (Clarify_tac 1);
  by (assume_tac 1);
 by (stac (prem RS is_maxsplitter_reducing RS chop_rule) 1);
- by (simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem]
+by (simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem]
                         addsplits [split_split]) 1);
 by (Clarify_tac 1);
-by (rtac conjI 1);
- by (Clarify_tac 1);
- by (exhaust_tac "yss" 1);
-  by (Asm_simp_tac 1);
+by(rename_tac "xs1 ys1 xss1 ys" 1);
+by(split_asm_tac [split_list_case_asm] 1);
  by (Asm_full_simp_tac 1);
  by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
  by (blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
-by (exhaust_tac "yss" 1);
- by (Asm_full_simp_tac 1);
+by (rtac conjI 1);
+ by (Clarify_tac 1);
  by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
  by (blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
 by (Clarify_tac 1);
-by (Asm_full_simp_tac 1);
-by (subgoal_tac "x=a" 1);
- by (Clarify_tac 1);
+by(rename_tac "us uss" 1);
+by (subgoal_tac "xs1=us" 1);
  by (Asm_full_simp_tac 1);
-by (rotate_tac ~2 1);
 by (Asm_full_simp_tac 1);
 by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
 by (blast_tac (claset() addIs [prefix_append RS iffD2,prefix_antisym]) 1);