equal
deleted
inserted
replaced
1 \documentclass[11pt,a4paper]{article} |
|
2 \usepackage{isabelle,isabellesym,pdfsetup} |
|
3 |
|
4 %for best-style documents ... |
|
5 \urlstyle{rm} |
|
6 %\isabellestyle{it} |
|
7 |
|
8 \newtheorem{Exercise}{Exercise}[section] |
|
9 \newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}} |
|
10 |
|
11 \begin{document} |
|
12 |
|
13 \title{A Compact Overview of Isabelle/HOL} |
|
14 \author{Tobias Nipkow} |
|
15 \date{} |
|
16 \maketitle |
|
17 |
|
18 \noindent |
|
19 This document is a very compact introduction to the proof assistant |
|
20 Isabelle/HOL and is based directly on the published tutorial~\cite{LNCS2283} |
|
21 where full explanations and a wealth of additional material can be found. |
|
22 |
|
23 While reading this document it is recommended to single-step through the |
|
24 corresponding theories using Isabelle/HOL to follow the proofs. |
|
25 |
|
26 \section{Functional Programming/Modelling} |
|
27 |
|
28 \subsection{An Introductory Theory} |
|
29 \input{FP0.tex} |
|
30 |
|
31 \subsection{More Constructs} |
|
32 \input{FP1.tex} |
|
33 |
|
34 \input{RECDEF.tex} |
|
35 |
|
36 \input{Rules.tex} |
|
37 |
|
38 \input{Sets.tex} |
|
39 |
|
40 \input{Ind.tex} |
|
41 |
|
42 %\input{Isar.tex} |
|
43 |
|
44 %%% Local Variables: |
|
45 %%% mode: latex |
|
46 %%% TeX-master: "root" |
|
47 %%% End: |
|
48 |
|
49 |
|
50 \bibliographystyle{plain} |
|
51 \bibliography{root} |
|
52 |
|
53 \end{document} |
|