1\documentclass[11pt,a4paper]{report}
2
3\input{prelude}
4
5\begin{document}
6
7\title{How to Prove it in Isabelle/HOL}
8%\subtitle{\includegraphics[scale=.7]{isabelle_hol}}
9\author{Tobias Nipkow}
10\maketitle
11
12
13\begin{abstract}
14  How does one perform induction on the length of a list? How are numerals
15  converted into \isa{Suc} terms? How does one prove equalities in rings
16  and other algebraic structures?
17
18  This document is a collection of practical hints and techniques for dealing
19  with specific frequently occurring situations in proofs in Isabelle/HOL.
20  Not arbitrary proofs but proofs that refer to material that is part of
21  \isa{Main} or \isa{Complex\_Main}.
22
23  This is \emph{not} an introduction to
24\begin{itemize}
25\item proofs in general; for that see mathematics or logic books.
26\item Isabelle/HOL and its proof language; for that see the tutorial
27  \cite{ProgProve} or the reference manual~\cite{IsarRef}.
28\item the contents of theory \isa{Main}; for that see the overview
29  \cite{Main}.
30\end{itemize}
31\end{abstract}
32
33\setcounter{tocdepth}{1}
34\tableofcontents
35
36\input{How_to_Prove_it.tex}
37
38\bibliographystyle{plain}
39\bibliography{root}
40
41%\printindex
42
43\end{document}
44