diff -r d9be8bc5624e -r 3ccaa11b6df9 lib/Tools/document
--- a/lib/Tools/document	Thu Oct 14 15:03:34 1999 +0200
+++ b/lib/Tools/document	Thu Oct 14 15:04:36 1999 +0200
@@ -13,7 +13,8 @@
   echo "Usage: $PRG [OPTIONS] [DIR]"
   echo
   echo "  Options are:"
-  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf"
+  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,"
+  echo "                 ps.gz, pdf"
   echo
   echo "  Prepare the theory session document in DIR (default '.')"
   echo "  producing the specified output format."
@@ -92,7 +93,11 @@
   RC=$?   #FIXME !??
 elif [ "$OUTFORMAT" = pdf ]; then
   pre_latex pdf && \
-  $ISATOOL latex -o pdf
+  $ISATOOL latex -o pdf && \
+  { if [ -n "$ISABELLE_THUMBPDF" ]; then
+      $ISATOOL latex -o png && \
+      $ISATOOL latex -o pdf
+    fi; }
   RC=$?
 else
   pre_latex dvi && \