# HG changeset patch # User nipkow # Date 1089991914 -7200 # Node ID 1ad0b310bc54d28ab44b6f61841045803afa15ce # Parent 405be2b48f5bb5b9d8a67e62f239cdbe7cdd0ffd Created. diff -r 405be2b48f5b -r 1ad0b310bc54 src/HOL/Complex/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Complex/document/root.tex Fri Jul 16 17:31:54 2004 +0200 @@ -0,0 +1,32 @@ + +% $Id$ + +\documentclass[11pt,a4paper]{article} +\usepackage{graphicx,isabelle,isabellesym,latexsym} +\usepackage[latin1]{inputenc} +\usepackage{pdfsetup} + +\urlstyle{rm} +\isabellestyle{it} +\pagestyle{myheadings} + +\begin{document} + +\title{Isabelle/HOL-Complex --- Higher-Order Logic with Complex Numbers} +\maketitle + +\tableofcontents + +\begin{center} + \includegraphics[scale=0.3]{session_graph} +\end{center} + +\newpage + +\renewcommand{\isamarkupheader}[1]% +{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}} + +\parindent 0pt\parskip 0.5ex +\input{session} + +\end{document}