src/HOL/Examples/document/root.tex
author wenzelm
Tue, 09 Mar 2021 21:11:05 +0100
changeset 73404 299f6a8faccc
parent 72320 c695d0b89586
child 74889 7dbac7d3cdab
permissions -rw-r--r--
proper type-setting of cartouches (requires T1); \usepackage[T1]{fontenc} is default for mkroot; \usepackage[utf8]{inputenc} is obsolete in lualatex;
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}
72320
c695d0b89586 more standard and more robust, following hints on the Net;
wenzelm
parents: 71929
diff changeset
     2
\usepackage[T1]{fontenc}
71925
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
     3
\usepackage[only,bigsqcap]{stmaryrd}
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
     4
\usepackage{ifthen,proof,amssymb,isabelle,isabellesym}
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
     5
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
     6
\isabellestyle{literal}
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
     7
\usepackage{pdfsetup}\urlstyle{rm}
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
     8
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
\hyphenation{Isabelle}
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    11
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    12
\begin{document}
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    13
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    14
\title{Notable Examples in Isabelle/HOL}
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    15
\maketitle
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    16
71929
73ff22f99d38 tuned document;
wenzelm
parents: 71925
diff changeset
    17
\tableofcontents
73ff22f99d38 tuned document;
wenzelm
parents: 71925
diff changeset
    18
71925
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    19
\parindent 0pt \parskip 0.5ex
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    20
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    21
\input{session}
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    22
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    23
\bibliographystyle{abbrv}
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    24
\bibliography{root}
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    25
bf085daea304 clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
diff changeset
    26
\end{document}