# HG changeset patch
# User huffman
# Date 1221839644 -7200
# Node ID 107ba67497a1f825f0640e1b61864eeeefebd614
# Parent  9efd7d4fa2f27ec5f93106bacfdb7b4589bcec3a
add theory graph to ZF document

diff -r 9efd7d4fa2f2 -r 107ba67497a1 src/ZF/IsaMakefile
--- 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
diff -r 9efd7d4fa2f2 -r 107ba67497a1 src/ZF/document/root.tex
--- 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