diff -r 29311d81954e -r feae7b5fd425 src/HOL/List.thy
--- 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