equal
deleted
inserted
replaced
3 \usepackage{isabelle,isabellesym,pdfsetup} |
3 \usepackage{isabelle,isabellesym,pdfsetup} |
4 |
4 |
5 %for best-style documents ... |
5 %for best-style documents ... |
6 \urlstyle{rm} |
6 \urlstyle{rm} |
7 %\isabellestyle{it} |
7 %\isabellestyle{it} |
|
8 |
|
9 \newcommand{\tweakskip}{\vspace{-\medskipamount}} |
|
10 \newcommand{\Tweakskip}{\tweakskip\tweakskip} |
|
11 |
|
12 \pagestyle{plain} |
8 |
13 |
9 \begin{document} |
14 \begin{document} |
10 |
15 |
11 \title{A Compact Introduction to Structured Proofs in Isar/HOL} |
16 \title{A Compact Introduction to Structured Proofs in Isar/HOL} |
12 \author{Tobias Nipkow} |
17 \author{Tobias Nipkow} |
16 \maketitle |
21 \maketitle |
17 |
22 |
18 \begin{abstract} |
23 \begin{abstract} |
19 Isar is an extension of the theorem prover Isabelle with a language |
24 Isar is an extension of the theorem prover Isabelle with a language |
20 for writing human-readable structured proofs. This paper is an |
25 for writing human-readable structured proofs. This paper is an |
21 introduction to the basic constructs of this language. It is aimed |
26 introduction to the basic constructs of this language. |
22 at potential users of Isar but also discusses the design rationals |
27 % It is aimed at potential users of Isar |
23 behind the language and its constructs. |
28 % but also discusses the design rationals |
|
29 % behind the language and its constructs. |
24 \end{abstract} |
30 \end{abstract} |
25 |
31 |
26 \input{intro.tex} |
32 \input{intro.tex} |
27 \input{Logic.tex} |
33 \input{Logic.tex} |
|
34 \Tweakskip\Tweakskip |
28 \input{Induction.tex} |
35 \input{Induction.tex} |
29 |
36 |
30 %\input{Isar.tex} |
37 \Tweakskip |
31 |
38 \Tweakskip |
32 %%% Local Variables: |
|
33 %%% mode: latex |
|
34 %%% TeX-master: "root" |
|
35 %%% End: |
|
36 |
|
37 {\small |
|
38 \paragraph{Acknowledgment} |
|
39 I am deeply indebted to Markus Wenzel for conceiving Isar. Clemens Ballarin, |
|
40 Gertrud Bauer, Stefan Berghofer, Gerwin Klein, Norbert Schirmer and |
|
41 Markus Wenzel commented on and improved this document. |
|
42 } |
|
43 |
|
44 \begingroup |
39 \begingroup |
45 \bibliographystyle{plain} \small\raggedright\frenchspacing |
40 \bibliographystyle{plain} \small\raggedright\frenchspacing |
46 \bibliography{root} |
41 \bibliography{root} |
47 \endgroup |
42 \endgroup |
48 |
43 |