| changeset 7028 | 6ea3b385e731 |
| parent 6831 | 799859f2e657 |
| child 7032 | d6efb3b8e669 |
--- 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";