--- a/src/ZF/IsaMakefile Fri Sep 19 09:41:17 2008 +0200
+++ b/src/ZF/IsaMakefile Fri Sep 19 17:54:04 2008 +0200
@@ -40,7 +40,7 @@
Tools/primrec_package.ML Tools/typechk.ML Trancl.thy Univ.thy WF.thy \
ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy ind_syntax.ML \
int_arith.ML pair.thy simpdata.ML upair.thy
- @$(ISATOOL) usedir -b -r $(OUT)/FOL ZF
+ @$(ISATOOL) usedir -b -g true -r $(OUT)/FOL ZF
## ZF-AC
--- a/src/ZF/document/root.tex Fri Sep 19 09:41:17 2008 +0200
+++ b/src/ZF/document/root.tex Fri Sep 19 17:54:04 2008 +0200
@@ -1,6 +1,6 @@
\documentclass[11pt,a4paper]{article}
-\usepackage{isabelle,isabellesym}
+\usepackage{graphicx,isabelle,isabellesym}
% further packages required for unusual symbols (see also isabellesym.sty)
%\usepackage{latexsym}
@@ -29,6 +29,15 @@
\tableofcontents
+\begin{center}
+ \includegraphics[width=\textwidth,height=\textheight,keepaspectratio]{session_graph}
+\end{center}
+
+\newpage
+
+\renewcommand{\isamarkupheader}[1]%
+{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
+
\parindent 0pt\parskip 0.5ex
% include generated text of all theories