1\documentclass[envcountsame,envcountchap]{svmono}
2
3\input{prelude}
4
5\newif\ifsem
6
7\begin{document}
8
9\title{Programming and Proving in Isabelle/HOL}
10\subtitle{\includegraphics[scale=.7]{isabelle_hol}}
11\author{Tobias Nipkow}
12\maketitle
13
14\frontmatter%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
15
16\setcounter{tocdepth}{1}
17\tableofcontents
18
19
20\mainmatter%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
21
22%\part{Isabelle}
23
24\chapter{Introduction}
25\input{intro-isabelle.tex}
26
27\chapter{Programming and Proving}
28\label{sec:FP}
29\input{Basics.tex}
30\input{Bool_nat_list}
31\input{Types_and_funs}
32
33%\chapter{Case Study: IMP Expressions}
34%\label{sec:CaseStudyExp}
35%\input{../generated/Expressions}
36
37\chapter{Logic and Proof Beyond Equality}
38\label{ch:Logic}
39\input{Logic}
40
41\chapter{Isar: A Language for Structured Proofs}
42\label{ch:Isar}
43\input{Isar}
44
45\backmatter%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
46
47\bibliographystyle{plain}
48\bibliography{root}
49
50%\printindex
51
52\end{document}
53