# HG changeset patch
# User wenzelm
# Date 1573240326 -3600
# Node ID 907b7a6471a0d4125129dad40627bc1a09cc1f3f
# Parent  4b45d592ce290f7ec415792afd9a06398c866e3b
tuned proofs;

diff -r 4b45d592ce29 -r 907b7a6471a0 src/ZF/List.thy
--- a/src/ZF/List.thy	Fri Nov 08 19:06:50 2019 +0100
+++ b/src/ZF/List.thy	Fri Nov 08 20:12:06 2019 +0100
@@ -1123,14 +1123,13 @@
 apply (auto dest!: not_lt_imp_le simp add: diff_succ diff_is_0_iff)
 done
 
-lemma nth_upt [rule_format]:
-     "[| i \<in> nat; j \<in> nat; k \<in> nat |] ==> i #+ k < j \<longrightarrow> nth(k, upt(i,j)) = i #+ k"
+lemma nth_upt [simp]:
+     "[| i \<in> nat; j \<in> nat; k \<in> nat; i #+ k < j |] ==> nth(k, upt(i,j)) = i #+ k"
+apply (rotate_tac -1, erule rev_mp)
 apply (induct_tac "j", simp)
-apply (simp add: nth_append le_iff)
 apply (auto dest!: not_lt_imp_le
-            simp add: nth_append less_diff_conv add_commute)
+            simp add: nth_append le_iff less_diff_conv add_commute)
 done
-declare nth_upt [simp]
 
 lemma take_upt [rule_format]:
      "[| m \<in> nat; n \<in> nat |] ==>