src/HOL/document/root.tex
author wenzelm
Mon, 16 Nov 2020 22:21:40 +0100
changeset 72860 65554bac121b
parent 61977 f55f28132128
child 73656 299f6a8faccc
permissions -rw-r--r--
clarified document;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12033
69cb2059aadc document setup;
wenzelm
parents:
diff changeset
     1
\documentclass[11pt,a4paper]{article}
12410
ef373ec6ade8 include session graph;
wenzelm
parents: 12033
diff changeset
     2
\usepackage{graphicx,isabelle,isabellesym,latexsym}
61977
f55f28132128 proper latex setup;
wenzelm
parents: 58888
diff changeset
     3
\usepackage{amsmath}
15691
900cf45ff0a6 _(_|_) is now override_on
nipkow
parents: 15503
diff changeset
     4
\usepackage{amssymb}
40945
b8703f63bfb2 recoded latin1 as utf8;
wenzelm
parents: 30329
diff changeset
     5
\usepackage{textcomp}
30329
97ce36d801b6 added babel -- necessary for bind infix syntax
haftmann
parents: 28246
diff changeset
     6
\usepackage[english]{babel}
15503
38616a65bfbd fixed latex problems by including bigsqcap
nipkow
parents: 14706
diff changeset
     7
\usepackage[only,bigsqcap]{stmaryrd}
40945
b8703f63bfb2 recoded latin1 as utf8;
wenzelm
parents: 30329
diff changeset
     8
\usepackage[utf8]{inputenc}
12033
69cb2059aadc document setup;
wenzelm
parents:
diff changeset
     9
\usepackage{pdfsetup}
69cb2059aadc document setup;
wenzelm
parents:
diff changeset
    10
69cb2059aadc document setup;
wenzelm
parents:
diff changeset
    11
\urlstyle{rm}
69cb2059aadc document setup;
wenzelm
parents:
diff changeset
    12
\isabellestyle{it}
14608
9f9d651d676b more elaborate header markup;
wenzelm
parents: 12737
diff changeset
    13
\pagestyle{myheadings}
12033
69cb2059aadc document setup;
wenzelm
parents:
diff changeset
    14
69cb2059aadc document setup;
wenzelm
parents:
diff changeset
    15
\begin{document}
69cb2059aadc document setup;
wenzelm
parents:
diff changeset
    16
69cb2059aadc document setup;
wenzelm
parents:
diff changeset
    17
\title{Isabelle/HOL --- Higher-Order Logic}
69cb2059aadc document setup;
wenzelm
parents:
diff changeset
    18
\maketitle
69cb2059aadc document setup;
wenzelm
parents:
diff changeset
    19
69cb2059aadc document setup;
wenzelm
parents:
diff changeset
    20
\tableofcontents
69cb2059aadc document setup;
wenzelm
parents:
diff changeset
    21
12410
ef373ec6ade8 include session graph;
wenzelm
parents: 12033
diff changeset
    22
\begin{center}
17159
d5060118122e tuned size of included graph;
wenzelm
parents: 16764
diff changeset
    23
  \includegraphics[width=\textwidth,height=\textheight,keepaspectratio]{session_graph}
12410
ef373ec6ade8 include session graph;
wenzelm
parents: 12033
diff changeset
    24
\end{center}
ef373ec6ade8 include session graph;
wenzelm
parents: 12033
diff changeset
    25
ef373ec6ade8 include session graph;
wenzelm
parents: 12033
diff changeset
    26
\newpage
ef373ec6ade8 include session graph;
wenzelm
parents: 12033
diff changeset
    27
58888
9537bf1c4853 prefer \setisabellecontext;
wenzelm
parents: 40945
diff changeset
    28
\renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}}
14608
9f9d651d676b more elaborate header markup;
wenzelm
parents: 12737
diff changeset
    29
12033
69cb2059aadc document setup;
wenzelm
parents:
diff changeset
    30
\parindent 0pt\parskip 0.5ex
72860
65554bac121b clarified document;
wenzelm
parents: 61977
diff changeset
    31
\input{Code_Generator.tex}
12033
69cb2059aadc document setup;
wenzelm
parents:
diff changeset
    32
\input{session}
69cb2059aadc document setup;
wenzelm
parents:
diff changeset
    33
16764
ca81a99c5bc1 added Davenport reference
nipkow
parents: 15691
diff changeset
    34
\pagestyle{headings}
ca81a99c5bc1 added Davenport reference
nipkow
parents: 15691
diff changeset
    35
\bibliographystyle{abbrv}
ca81a99c5bc1 added Davenport reference
nipkow
parents: 15691
diff changeset
    36
\bibliography{root}
ca81a99c5bc1 added Davenport reference
nipkow
parents: 15691
diff changeset
    37
12033
69cb2059aadc document setup;
wenzelm
parents:
diff changeset
    38
\end{document}