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.
Modifid length_tl
authornipkow
Sun, 18 Jul 1999 11:06:08 +0200
changeset 7028 6ea3b385e731
parent 7027 ca0fbe679bbb
child 7029 08d4eb8500dd
Modifid length_tl
src/HOL/List.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/List.ML	Fri Jul 16 22:27:16 1999 +0200
+++ b/src/HOL/List.ML	Sun Jul 18 11:06:08 1999 +0200
@@ -87,7 +87,7 @@
 qed "length_rev";
 Addsimps [length_rev];
 
-Goal "xs ~= [] ==> length(tl xs) = (length xs) - 1";
+Goal "length(tl xs) = (length xs) - 1";
 by (exhaust_tac "xs" 1);
 by Auto_tac;
 qed "length_tl";
isabelle