src/HOL/document/root.tex
author wenzelm
Thu May 24 17:25:53 2012 +0200 (2012-05-24)
changeset 47988 e4b69e10b990
parent 40945 b8703f63bfb2
child 58888 9537bf1c4853
permissions -rw-r--r--
tuned proofs;
wenzelm@12033
     1
wenzelm@12033
     2
\documentclass[11pt,a4paper]{article}
wenzelm@12410
     3
\usepackage{graphicx,isabelle,isabellesym,latexsym}
nipkow@15691
     4
\usepackage{amssymb}
wenzelm@40945
     5
\usepackage{textcomp}
haftmann@30329
     6
\usepackage[english]{babel}
nipkow@15503
     7
\usepackage[only,bigsqcap]{stmaryrd}
wenzelm@40945
     8
\usepackage[utf8]{inputenc}
wenzelm@12033
     9
\usepackage{pdfsetup}
wenzelm@12033
    10
wenzelm@12033
    11
\urlstyle{rm}
wenzelm@12033
    12
\isabellestyle{it}
wenzelm@14608
    13
\pagestyle{myheadings}
wenzelm@12033
    14
wenzelm@12033
    15
\begin{document}
wenzelm@12033
    16
wenzelm@12033
    17
\title{Isabelle/HOL --- Higher-Order Logic}
wenzelm@12033
    18
\maketitle
wenzelm@12033
    19
wenzelm@12033
    20
\tableofcontents
wenzelm@12033
    21
wenzelm@12410
    22
\begin{center}
wenzelm@17159
    23
  \includegraphics[width=\textwidth,height=\textheight,keepaspectratio]{session_graph}
wenzelm@12410
    24
\end{center}
wenzelm@12410
    25
wenzelm@12410
    26
\newpage
wenzelm@12410
    27
wenzelm@14608
    28
\renewcommand{\isamarkupheader}[1]%
wenzelm@14706
    29
{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
wenzelm@14608
    30
wenzelm@12033
    31
\parindent 0pt\parskip 0.5ex
wenzelm@12033
    32
\input{session}
wenzelm@12033
    33
nipkow@16764
    34
\pagestyle{headings}
nipkow@16764
    35
\bibliographystyle{abbrv}
nipkow@16764
    36
\bibliography{root}
nipkow@16764
    37
wenzelm@12033
    38
\end{document}