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