src/HOL/Real/HahnBanach/ROOT.ML
changeset 7927 b50446a33c16
parent 7808 fd019ac3485f
child 7978 1b99ee57d131
--- a/src/HOL/Real/HahnBanach/ROOT.ML	Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/ROOT.ML	Mon Oct 25 19:24:43 1999 +0200
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Gertrud Bauer, TU Munich
 
-The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).
+The Hahn-Banach theorem for real vector spaces (Isabelle/Isar).
 *)
 
 time_use_thy "Bounds";