doc-src/ProgProve/prog-prove.tex
author wenzelm
Tue, 22 May 2012 19:02:17 +0200
changeset 47885 b987aa8b9310
parent 47269 29aa0c071875
permissions -rw-r--r--
Added tag Isabelle2012 for changeset 21c42b095c84

\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}