doc-src/ProgProve/prog-prove.tex
author wenzelm
Sun, 20 May 2012 11:34:33 +0200
changeset 47884 21c42b095c84
parent 47269 29aa0c071875
permissions -rw-r--r--
try to avoid races again (cf. 8c37cb84065f and fd3a36e48b09);

\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{Thys/document/Basics.tex}
\input{Thys/document/Bool_nat_list}
\input{Thys/document/Types_and_funs}

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

\chapter{Logic}
\label{ch:Logic}
\input{Thys/document/Logic}

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

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

\bibliographystyle{plain}
\bibliography{prog-prove}

%\printindex

\end{document}