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