| changeset 8982 | 4cb682fc083d |
| parent 8935 | 548901d05a0e |
| child 9003 | 3747ec2aeb86 |
--- 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);