Modifid length_tl
authornipkow
Sun Jul 18 11:06:08 1999 +0200 (1999-07-18)
changeset 70286ea3b385e731
parent 7027 ca0fbe679bbb
child 7029 08d4eb8500dd
Modifid length_tl
src/HOL/List.ML
     1.1 --- a/src/HOL/List.ML	Fri Jul 16 22:27:16 1999 +0200
     1.2 +++ b/src/HOL/List.ML	Sun Jul 18 11:06:08 1999 +0200
     1.3 @@ -87,7 +87,7 @@
     1.4  qed "length_rev";
     1.5  Addsimps [length_rev];
     1.6  
     1.7 -Goal "xs ~= [] ==> length(tl xs) = (length xs) - 1";
     1.8 +Goal "length(tl xs) = (length xs) - 1";
     1.9  by (exhaust_tac "xs" 1);
    1.10  by Auto_tac;
    1.11  qed "length_tl";