diff -r a9b8344f5196 -r 7eee8b2d2099 doc-src/ProgProve/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/ProgProve/document/root.tex	Mon Aug 27 22:00:04 2012 +0200
@@ -0,0 +1,52 @@
+\documentclass[envcountsame,envcountchap]{svmono}
+
+\input{prelude}
+
+\excludecomment{sem}
+
+\begin{document}
+
+\title{Programming and Proving in Isabelle/HOL}
+\subtitle{\includegraphics[scale=.7]{isabelle_hol}}
+\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}
+\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}