--- a/src/HOL/List.ML Fri Jan 08 14:02:04 1999 +0100
+++ b/src/HOL/List.ML Sat Jan 09 15:24:11 1999 +0100
@@ -906,20 +906,10 @@
by(induct_tac "j" 1);
by(Simp_tac 1);
by(asm_simp_tac (simpset() addsimps [nth_append,less_diff_conv]@add_ac) 1);
-br conjI 1;
- by(Clarify_tac 1);
- bd add_lessD1 1;
- by(Simp_tac 1);
-by(Clarify_tac 1);
-br conjI 1;
- by(Clarify_tac 1);
- by(subgoal_tac "n=i+k" 1);
- by(Asm_full_simp_tac 1);
- by(Simp_tac 1);
by(Clarify_tac 1);
by(subgoal_tac "n=i+k" 1);
- by(Asm_full_simp_tac 1);
-by(Simp_tac 1);
+ by(Asm_simp_tac 2);
+by(Asm_simp_tac 1);
qed_spec_mp "nth_upt";
Addsimps [nth_upt];