# HG changeset patch
# User paulson
# Date 959357034 -7200
# Node ID 4cb682fc083d6eb907c54c2625a344d41cc9d0cb
# Parent  fe1f3d52e0277ebd046a1d82383a71864a7c4e22
renamed upt_Suc, since that name is needed for its primrec rule

diff -r fe1f3d52e027 -r 4cb682fc083d src/HOL/List.ML
--- a/src/HOL/List.ML	Fri May 26 18:03:25 2000 +0200
+++ b/src/HOL/List.ML	Fri May 26 18:03:54 2000 +0200
@@ -1176,9 +1176,10 @@
 qed "upt_conv_Nil";
 Addsimps [upt_conv_Nil];
 
+(*Only needed if upt_Suc is deleted from the simpset*)
 Goal "i<=j ==> [i..(Suc j)(] = [i..j(]@[j]";
 by (Asm_simp_tac 1);
-qed "upt_Suc";
+qed "upt_Suc_append";
 
 Goal "i<j ==> [i..j(] = i#[Suc i..j(]";
 by (rtac trans 1);