# HG changeset patch # User nipkow # Date 932288768 -7200 # Node ID 6ea3b385e7317b0aab2d63ee66671f0de808800a # Parent ca0fbe679bbbd50a8cf82132d02299a7152522d0 Modifid length_tl diff -r ca0fbe679bbb -r 6ea3b385e731 src/HOL/List.ML --- 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";