src/HOL/List.ML
changeset 4628 0c7e97836e3c
parent 4605 579e0ef2df6b
child 4643 1b40fcac5a09
     1.1 --- a/src/HOL/List.ML	Thu Feb 12 17:43:53 1998 +0100
     1.2 +++ b/src/HOL/List.ML	Thu Feb 12 17:53:05 1998 +0100
     1.3 @@ -84,7 +84,7 @@
     1.4  qed "length_rev";
     1.5  Addsimps [length_rev];
     1.6  
     1.7 -goal List.thy "!!xs. xs ~= [] ==> length(tl xs) = pred(length xs)";
     1.8 +goal List.thy "!!xs. xs ~= [] ==> length(tl xs) = (length xs) - 1";
     1.9  by (exhaust_tac "xs" 1);
    1.10  by (ALLGOALS Asm_full_simp_tac);
    1.11  qed "length_tl";