Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
renamed upt_Suc, since that name is needed for its primrec rule
authorpaulson
Fri, 26 May 2000 18:03:54 +0200
changeset 8982 4cb682fc083d
parent 8981 fe1f3d52e027
child 8983 15bd7d568fb2
renamed upt_Suc, since that name is needed for its primrec rule
src/HOL/List.ML file | annotate | diff | comparison | revisions 
--- 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);
isabelle