src/Doc/Prog_Prove/document/root.tex

tuned whitespace;

\documentclass[envcountsame,envcountchap]{svmono}

\input{prelude}

\newif\ifsem

\begin{document}

\title{Programming and Proving in Isabelle/HOL}
\subtitle{\includegraphics[scale=.7]{isabelle_logo}}
\author{Tobias Nipkow}
\maketitle

\frontmatter%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\setcounter{tocdepth}{1}
\tableofcontents


\mainmatter%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\part{Isabelle}

\chapter{Introduction}
\input{intro-isabelle.tex}

\chapter{Programming and Proving}
\label{sec:FP}
\input{Basics.tex}
\input{Bool_nat_list}
\input{Types_and_funs}

%\chapter{Case Study: IMP Expressions}
%\label{sec:CaseStudyExp}
%\input{../generated/Expressions}

\chapter{Logic and Proof Beyond Equality}
\label{ch:Logic}
\input{Logic}

\chapter{Isar: A Language for Structured Proofs}
\label{ch:Isar}
\input{Isar}

\backmatter%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\bibliographystyle{plain}
\bibliography{root}

%\printindex

\end{document}