changeset 14589 | feae7b5fd425 |
parent 14565 | c6dc17aab88a |
child 14591 | 7be4d5dadf15 |
--- a/src/HOL/List.thy Fri Apr 16 12:09:31 2004 +0200 +++ b/src/HOL/List.thy Fri Apr 16 13:51:04 2004 +0200 @@ -76,7 +76,7 @@ text {* - Function @{text size} is overloaded for all datatypes.Users may + Function @{text size} is overloaded for all datatypes. Users may refer to the list version as @{text length}. *} syntax length :: "'a list => nat" @@ -795,7 +795,6 @@ by(simp add:last_append) - lemma length_butlast [simp]: "length (butlast xs) = length xs - 1" by (induct xs rule: rev_induct) auto