author | ballarin |
Sat, 21 Nov 2009 18:33:55 +0100 | |
changeset 33839 | beae0c7a748d |
parent 33838 | a3166a169793 |
child 40405 | 42671298f037 |
permissions | -rw-r--r-- |
27063 | 1 |
\documentclass[11pt,a4paper]{article} |
14586 | 2 |
\usepackage{amsmath} |
27082
9102d87efd3d
tikz: change to pgfsys-dvi.def for plain dvi output;
wenzelm
parents:
27078
diff
changeset
|
3 |
\usepackage{ifpdf} |
9102d87efd3d
tikz: change to pgfsys-dvi.def for plain dvi output;
wenzelm
parents:
27078
diff
changeset
|
4 |
\ifpdf\relax\else\def\pgfsysdriver{pgfsys-dvi.def}\fi |
27063 | 5 |
\usepackage{tikz} |
6 |
\usepackage{subfigure} |
|
27078 | 7 |
\usepackage{../../../isabelle,../../../isabellesym} |
27063 | 8 |
\usepackage{verbatim} |
32981 | 9 |
\usepackage{alltt} |
14586 | 10 |
\usepackage{array} |
11 |
||
27063 | 12 |
\usepackage{amssymb} |
13 |
||
27078 | 14 |
\usepackage{../../../pdfsetup} |
27063 | 15 |
|
27078 | 16 |
\isadroptag{theory} |
27063 | 17 |
\isafoldtag{proof} |
18 |
||
19 |
% urls in roman style, theory text in typewriter |
|
14586 | 20 |
\urlstyle{rm} |
21 |
\isabellestyle{tt} |
|
27063 | 22 |
|
14586 | 23 |
|
24 |
\begin{document} |
|
25 |
||
33838
a3166a169793
Publication details and minor correction of the text.
ballarin
parents:
32983
diff
changeset
|
26 |
\title{Tutorial to Locales and Locale Interpretation% |
a3166a169793
Publication details and minor correction of the text.
ballarin
parents:
32983
diff
changeset
|
27 |
\thanks{Published in L.~Lamb\'an, A.~Romero, J.~Rubio, editors, {\em Contribuciones Cient\'{\i}ficas en honor de Mirian Andr\'es.} Servicio de Publicaciones de la Universidad de La Rioja, Logro\~no, Spain, 2010. Reproduced by permission.}} |
27063 | 28 |
\author{Clemens Ballarin} |
14586 | 29 |
\date{} |
30 |
||
31 |
\maketitle |
|
32 |
||
33 |
\begin{abstract} |
|
32983 | 34 |
Locales are Isabelle's approach for dealing with parametric |
35 |
theories. They have been designed as a module system for a |
|
36 |
theorem prover that can adequately represent the complex |
|
37 |
inter-dependencies between structures found in abstract algebra, but |
|
38 |
have proven fruitful also in other applications --- for example, |
|
39 |
software verification. |
|
27063 | 40 |
|
32983 | 41 |
Both design and implementation of locales have evolved considerably |
42 |
since Kamm\"uller did his initial experiments. Today, locales |
|
43 |
are a simple yet powerful extension of the Isar proof language. |
|
44 |
The present tutorial covers all major facilities of locales. It is |
|
45 |
intended for locale novices; familiarity with Isabelle and Isar is |
|
46 |
presumed. |
|
14586 | 47 |
\end{abstract} |
48 |
||
49 |
\parindent 0pt\parskip 0.5ex |
|
50 |
||
51 |
\input{session} |
|
52 |
||
27063 | 53 |
\bibliographystyle{abbrv} |
14586 | 54 |
\bibliography{root} |
55 |
||
56 |
\end{document} |
|
27063 | 57 |
|
58 |
%%% Local Variables: |
|
59 |
%%% mode: latex |
|
60 |
%%% TeX-master: t |
|
61 |
%%% End: |