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