src/HOL/HOLCF/document/root.tex
changeset 40774 0437dbc127b3
parent 35901 12f09bf2c77f
child 40945 b8703f63bfb2
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/HOLCF/document/root.tex	Sat Nov 27 16:08:10 2010 -0800
     1.3 @@ -0,0 +1,35 @@
     1.4 +
     1.5 +% HOLCF/document/root.tex
     1.6 +
     1.7 +\documentclass[11pt,a4paper]{article}
     1.8 +\usepackage{graphicx,isabelle,isabellesym,latexsym}
     1.9 +\usepackage[only,bigsqcap]{stmaryrd}
    1.10 +\usepackage[latin1]{inputenc}
    1.11 +\usepackage{pdfsetup}
    1.12 +
    1.13 +\urlstyle{rm}
    1.14 +\isabellestyle{it}
    1.15 +\pagestyle{myheadings}
    1.16 +\newcommand{\isasymas}{\textsf{as}}
    1.17 +\newcommand{\isasymlazy}{\isamath{\sim}}
    1.18 +
    1.19 +\begin{document}
    1.20 +
    1.21 +\title{Isabelle/HOLCF --- Higher-Order Logic of Computable Functions}
    1.22 +\maketitle
    1.23 +
    1.24 +\tableofcontents
    1.25 +
    1.26 +\begin{center}
    1.27 +  \includegraphics[scale=0.45]{session_graph}
    1.28 +\end{center}
    1.29 +
    1.30 +\newpage
    1.31 +
    1.32 +\renewcommand{\isamarkupheader}[1]%
    1.33 +{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
    1.34 +
    1.35 +\parindent 0pt\parskip 0.5ex
    1.36 +\input{session}
    1.37 +
    1.38 +\end{document}