doc-src/Locales/Locales/document/root.tex
author ballarin
Sat, 17 Oct 2009 22:58:18 +0200
changeset 32983 a6914429005b
parent 32981 0114e04a0d64
child 33838 a3166a169793
permissions -rw-r--r--
Finished revisions of locales tutorial.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
     1
\documentclass[11pt,a4paper]{article}
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     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
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
     5
\usepackage{tikz}
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
     6
\usepackage{subfigure}
27078
41483ec1b5b6 work within *this* directory;
wenzelm
parents: 27068
diff changeset
     7
\usepackage{../../../isabelle,../../../isabellesym}
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
     8
\usepackage{verbatim}
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30779
diff changeset
     9
\usepackage{alltt}
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    10
\usepackage{array}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    11
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    12
\usepackage{amssymb}
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    13
27078
41483ec1b5b6 work within *this* directory;
wenzelm
parents: 27068
diff changeset
    14
\usepackage{../../../pdfsetup}
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    15
27078
41483ec1b5b6 work within *this* directory;
wenzelm
parents: 27068
diff changeset
    16
\isadroptag{theory}
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    17
\isafoldtag{proof}
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    18
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    19
% urls in roman style, theory text in typewriter
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    20
\urlstyle{rm}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    21
\isabellestyle{tt}
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    22
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    23
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    24
\begin{document}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    25
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    26
\title{Tutorial to Locales and Locale Interpretation}
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    27
\author{Clemens Ballarin}
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    28
\date{}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    29
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    30
\maketitle
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    31
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    32
\begin{abstract}
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    33
  Locales are Isabelle's approach for dealing with parametric
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    34
  theories.  They have been designed as a module system for a
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    35
  theorem prover that can adequately represent the complex
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    36
  inter-dependencies between structures found in abstract algebra, but
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    37
  have proven fruitful also in other applications --- for example,
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    38
  software verification.
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    39
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    40
  Both design and implementation of locales have evolved considerably
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    41
  since Kamm\"uller did his initial experiments.  Today, locales
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    42
  are a simple yet powerful extension of the Isar proof language.
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    43
  The present tutorial covers all major facilities of locales.  It is
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    44
  intended for locale novices; familiarity with Isabelle and Isar is
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    45
  presumed.
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    46
\end{abstract}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    47
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    48
\parindent 0pt\parskip 0.5ex
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    49
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    50
\input{session}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    51
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    52
\newpage
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    53
\bibliographystyle{abbrv}
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    54
\bibliography{root}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    55
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    56
\end{document}
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    57
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    58
%%% Local Variables:
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    59
%%% mode: latex
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    60
%%% TeX-master: t
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    61
%%% End: