equal
deleted
inserted
replaced
|
1 \documentclass[leqno]{article} |
|
2 \usepackage{isabelle,isabellesym} |
|
3 |
|
4 \usepackage{amsmath} |
|
5 \usepackage{amssymb} |
|
6 \usepackage{array} |
|
7 |
|
8 % this should be the last package used |
|
9 \usepackage{pdfsetup} |
|
10 |
|
11 \urlstyle{rm} |
|
12 \isabellestyle{tt} |
|
13 %\renewcommand{\isacharunderscore}{\_}% |
|
14 % the latter is not necessary with \isabellestyle{tt} |
|
15 |
|
16 \begin{document} |
|
17 |
|
18 \title{Locales and Locale Expressions in Isabelle/Isar} |
|
19 \author{Clemens Ballarin \\ |
|
20 Fakult\"at f\"ur Informatik \\ Technische Universit\"at M\"unchen \\ |
|
21 85748 Garching, Germany \\ |
|
22 ballarin@in.tum.de} |
|
23 \date{} |
|
24 |
|
25 \maketitle |
|
26 |
|
27 \begin{abstract} |
|
28 Locales provide a module system for the Isabelle proof assistant. |
|
29 Recently, locales have been ported to the new Isar format for |
|
30 structured proofs. At the same time, they have been extended by |
|
31 locale expressions, a language for composing locale specifications, |
|
32 and by structures, which provide syntax for algebraic structures. |
|
33 The present paper presents both and is suitable as a tutorial to |
|
34 locales in Isar, because it covers both basics and recent |
|
35 extensions, and contains many examples. |
|
36 \end{abstract} |
|
37 |
|
38 %\tableofcontents |
|
39 |
|
40 \parindent 0pt\parskip 0.5ex |
|
41 |
|
42 % include generated text of all theories |
|
43 \input{session} |
|
44 |
|
45 \bibliographystyle{plain} |
|
46 \bibliography{root} |
|
47 |
|
48 \end{document} |