diff --git a/ChangeLog b/ChangeLog
index 8b1383be2..9bb560d70 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,7 @@
 2005-01-29  Alexandre Duret-Lutz  <adl@gnu.org>
 
+	* doc/mainpage.dox: More text, and a link to "Modules".
+
 	* src/tgbatest/ltl2tgba.cc (main): Silence the "filename.tgba read"
 	message if -0 is used.
 
diff --git a/doc/mainpage.dox b/doc/mainpage.dox
index 2f9b523cf..14a55b0c2 100644
--- a/doc/mainpage.dox
+++ b/doc/mainpage.dox
@@ -1,6 +1,21 @@
 /// \mainpage
 ///
-/// This main page has yet to be written.
+/// \section overview The Spot Library
+///
+/// Spot is a model-checking library.  It provides algorithms and data
+/// structures to implement the automata-theoretic approach to
+/// model-checking.
+///
+/// See <a href="http://spot.lip6.fr/">spot.lip6.fr</a> for more
+/// information about this project.
+///
+/// \section thisdoc This Document
+///
+/// This document describes all the public data structures and functions
+/// of Spot.  This aims to be a reference manual, not a tutorial.
+///
+/// If you are new to this manual, start with <a href="modules.html">the
+/// module page</a>.  This is what looks the closest to a table of contents.
 ///
 /// \section pointers Handy starting points
 ///
@@ -11,6 +26,6 @@
 ///                         Generalized Büchi Automaton.
 /// \li spot::ltl_to_tgba_fm  Convert a spot::ltl::formula into a
 ///                           spot::tgba.
-/// \li spot::ltl_to_tgba_lacim Likewise.
-
-
+/// \li spot::tgba_product    On-the-fly product of two spot::tgba.
+/// \li spot::emptiness_check Base class for all emptiness-check algorithms
+///                           (see also module \ref emptiness_check)