src/Doc/ProgProve/document/root.tex
author nipkow
Sun, 17 Mar 2013 20:29:26 +0100
changeset 51444 027cdce376d5
parent 51436 790310525e97
child 52782 b11d73dbfb76
permissions -rw-r--r--
tuned

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