author  nipkow 
Sun, 17 Mar 2013 20:29:26 +0100  
changeset 51444  027cdce376d5 
parent 51436  790310525e97 
child 52782  b11d73dbfb76 
permissions  rwrr 
47269  1 
\documentclass[envcountsame,envcountchap]{svmono} 
2 

3 
\input{prelude} 

4 

5 
\excludecomment{sem} 

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{introisabelle.tex} 

26 

27 
\chapter{Programming and Proving} 

28 
\label{sec:FP} 

48947
7eee8b2d2099
more standard document preparation within session context;
wenzelm
parents:
47269
diff
changeset

29 
\input{Basics.tex} 
7eee8b2d2099
more standard document preparation within session context;
wenzelm
parents:
47269
diff
changeset

30 
\input{Bool_nat_list} 
7eee8b2d2099
more standard document preparation within session context;
wenzelm
parents:
47269
diff
changeset

31 
\input{Types_and_funs} 
47269  32 

33 
%\chapter{Case Study: IMP Expressions} 

34 
%\label{sec:CaseStudyExp} 

35 
%\input{../generated/Expressions} 

36 

51444  37 
\chapter{Logic and Proof Beyond Equality} 
47269  38 
\label{ch:Logic} 
48947
7eee8b2d2099
more standard document preparation within session context;
wenzelm
parents:
47269
diff
changeset

39 
\input{Logic} 
47269  40 

41 
\chapter{Isar: A Language for Structured Proofs} 

42 
\label{ch:Isar} 

48947
7eee8b2d2099
more standard document preparation within session context;
wenzelm
parents:
47269
diff
changeset

43 
\input{Isar} 
47269  44 

45 
\backmatter%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

46 

47 
\bibliographystyle{plain} 

48947
7eee8b2d2099
more standard document preparation within session context;
wenzelm
parents:
47269
diff
changeset

48 
\bibliography{root} 
47269  49 

50 
%\printindex 

51 

52 
\end{document} 