renamed upt_Suc, since that name is needed for its primrec rule
authorpaulson
Fri May 26 18:03:54 2000 +0200 (2000-05-26)
changeset 89824cb682fc083d
parent 8981 fe1f3d52e027
child 8983 15bd7d568fb2
renamed upt_Suc, since that name is needed for its primrec rule
src/HOL/List.ML
     1.1 --- a/src/HOL/List.ML	Fri May 26 18:03:25 2000 +0200
     1.2 +++ b/src/HOL/List.ML	Fri May 26 18:03:54 2000 +0200
     1.3 @@ -1176,9 +1176,10 @@
     1.4  qed "upt_conv_Nil";
     1.5  Addsimps [upt_conv_Nil];
     1.6  
     1.7 +(*Only needed if upt_Suc is deleted from the simpset*)
     1.8  Goal "i<=j ==> [i..(Suc j)(] = [i..j(]@[j]";
     1.9  by (Asm_simp_tac 1);
    1.10 -qed "upt_Suc";
    1.11 +qed "upt_Suc_append";
    1.12  
    1.13  Goal "i<j ==> [i..j(] = i#[Suc i..j(]";
    1.14  by (rtac trans 1);