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