src/Doc/Isar_Ref/document/root.tex
author wenzelm
Mon, 22 Mar 2021 17:24:42 +0100
changeset 73467 090add96f5f9
parent 73446 d1c4c2395650
child 73723 1bbbaae6b5e3
permissions -rw-r--r--
more glyphs proposed by Simon Foster: 0x002713, 0x002717, 0x002af4, 0x002afb, 0x002afd; corresponding symbols and latex macros;

\documentclass[12pt,a4paper,fleqn]{report}
\usepackage[T1]{fontenc}
\usepackage{textcomp}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{wasysym}
\usepackage{eurosym}
\usepackage{pifont}
\usepackage[english]{babel}
\usepackage[only,bigsqcap,fatsemi,interleave,sslash]{stmaryrd}
\usepackage{graphicx}
\let\intorig=\int  %iman.sty redefines \int
\usepackage{iman,extra,isar,proof}
\usepackage[nohyphen,strings]{underscore}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{railsetup}
\usepackage{supertabular}
\usepackage{style}
\usepackage{pdfsetup}

\hyphenation{Isabelle}
\hyphenation{Isar}

\isadroptag{theory}
\title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
\author{\emph{Makarius Wenzel} \\[3ex]
  With Contributions by
  Clemens Ballarin,
  Stefan Berghofer, \\
  Jasmin Blanchette,
  Timothy Bourke,
  Lukas Bulwahn, \\
  Amine Chaieb,
  Lucas Dixon,
  Florian Haftmann, \\
  Brian Huffman,
  Lars Hupel,
  Gerwin Klein, \\
  Alexander Krauss,
  Ond\v{r}ej Kun\v{c}ar,
  Andreas Lochbihler, \\
  Tobias Nipkow,
  Lars Noschinski,
  David von Oheimb, \\
  Larry Paulson,
  Sebastian Skalberg, \\
  Christian Sternagel,
  Dmitriy Traytel
}

\makeindex

\chardef\charbackquote=`\`
\newcommand{\backquote}{\mbox{\tt\charbackquote}}


\begin{document}

\maketitle 

\pagenumbering{roman}
\chapter*{Preface}
\input{Preface.tex}
\tableofcontents
\listoffigures
\clearfirst

\part{Basic Concepts}
\input{Synopsis.tex}
\input{Framework.tex}
\input{First_Order_Logic.tex}
\part{General Language Elements}
\input{Outer_Syntax.tex}
\input{Document_Preparation.tex}
\input{Spec.tex}
\input{Proof.tex}
\input{Proof_Script.tex}
\input{Inner_Syntax.tex}
\input{Generic.tex}
\part{Isabelle/HOL}\label{part:hol}
\input{HOL_Specific.tex}

\part{Appendix}
\appendix
\input{Quick_Reference.tex}
\let\int\intorig
\input{Symbols.tex}

\begingroup
  \tocentry{\bibname}
  \bibliographystyle{abbrv} \small\raggedright\frenchspacing
  \bibliography{manual}
\endgroup

\tocentry{\indexname}
\printindex

\end{document}