src/HOL/Examples/document/root.tex
author paulson <lp15@cam.ac.uk>
Tue, 09 Jun 2020 12:13:15 +0100
changeset 71930 35a2ac83a262
parent 71929 73ff22f99d38
child 72320 c695d0b89586
permissions -rw-r--r--
New Ackermann development
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
71925
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
     1
\documentclass[11pt,a4paper]{article}
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
     2
\usepackage[utf8]{inputenc}
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
     3
\usepackage[T1]{fontenc}
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
     4
\usepackage[only,bigsqcap]{stmaryrd}
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
     5
\usepackage{ifthen,proof,amssymb,isabelle,isabellesym}
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
     6
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
     7
\isabellestyle{literal}
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
     8
\usepackage{pdfsetup}\urlstyle{rm}
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
     9
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    10
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    11
\hyphenation{Isabelle}
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    12
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    13
\begin{document}
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    14
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    15
\title{Notable Examples in Isabelle/HOL}
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    16
\maketitle
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    17
71929
73ff22f99d38 tuned document;
wenzelm
parents: 71925
diff changeset
    18
\tableofcontents
73ff22f99d38 tuned document;
wenzelm
parents: 71925
diff changeset
    19
71925
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    20
\parindent 0pt \parskip 0.5ex
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    21
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    22
\input{session}
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    23
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    24
\bibliographystyle{abbrv}
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    25
\bibliography{root}
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    26
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    27
\end{document}