# HG changeset patch
# User paulson
# Date 959858880 -7200
# Node ID 4382883421ecec0b050fcf8fef6396732e5bddee
# Parent  9dd0274f76afb155ed8ecd7f22f8a44a41911ef6
simplified the proof of nth_upt

diff -r 9dd0274f76af -r 4382883421ec src/HOL/List.ML
--- a/src/HOL/List.ML	Thu Jun 01 11:22:27 2000 +0200
+++ b/src/HOL/List.ML	Thu Jun 01 13:28:00 2000 +0200
@@ -1200,12 +1200,9 @@
 
 Goal "i+k < j --> [i..j(] ! k = i+k";
 by (induct_tac "j" 1);
- by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [nth_append,less_diff_conv]@add_ac) 1);
-by (Clarify_tac 1);
-by (subgoal_tac "n=i+k" 1);
- by (Asm_simp_tac 2);
-by (Asm_simp_tac 1);
+ by (asm_simp_tac (simpset() addsimps [less_Suc_eq, nth_append] 
+                             addsplits [nat_diff_split]) 2);
+by (Simp_tac 1);
 qed_spec_mp "nth_upt";
 Addsimps [nth_upt];