src/Doc/Locales/document/root.tex
author wenzelm
Sat, 05 Apr 2014 15:03:40 +0200
changeset 56421 1ffd7eaa778b
parent 48985 5386df44a037
child 57002 97a80d41a5ba
permissions -rw-r--r--
updated to jedit_build-20140405: Code2HTML.jar, CommonControls.jar, Console.jar, kappalayout.jar, Navigator.jar, SideKick.jar, doc with jEdit manuals (ant dist-manuals);
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}
48943
54da920baf38 more standard document preparation within session context;
wenzelm
parents: 42511
diff changeset
     3
\usepackage{isabelle,isabellesym}
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
     4
\usepackage{verbatim}
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 30779
diff changeset
     5
\usepackage{alltt}
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     6
\usepackage{array}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     7
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
     8
\usepackage{amssymb}
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
     9
48943
54da920baf38 more standard document preparation within session context;
wenzelm
parents: 42511
diff changeset
    10
\usepackage{pdfsetup}
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    11
40405
42671298f037 tweaked pdf setup to allow modification of \pdfminorversion;
wenzelm
parents: 33839
diff changeset
    12
\usepackage{ifpdf}
42671298f037 tweaked pdf setup to allow modification of \pdfminorversion;
wenzelm
parents: 33839
diff changeset
    13
\ifpdf\relax\else\def\pgfsysdriver{pgfsys-dvi.def}\fi
42671298f037 tweaked pdf setup to allow modification of \pdfminorversion;
wenzelm
parents: 33839
diff changeset
    14
\usepackage{tikz}
42671298f037 tweaked pdf setup to allow modification of \pdfminorversion;
wenzelm
parents: 33839
diff changeset
    15
\usepackage{subfigure}
42671298f037 tweaked pdf setup to allow modification of \pdfminorversion;
wenzelm
parents: 33839
diff changeset
    16
27078
41483ec1b5b6 work within *this* directory;
wenzelm
parents: 27068
diff changeset
    17
\isadroptag{theory}
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    18
\isafoldtag{proof}
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    19
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    20
% urls in roman style, theory text in typewriter
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    21
\urlstyle{rm}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    22
\isabellestyle{tt}
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    23
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    24
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    25
\begin{document}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    26
33838
a3166a169793 Publication details and minor correction of the text.
ballarin
parents: 32983
diff changeset
    27
\title{Tutorial to Locales and Locale Interpretation%
a3166a169793 Publication details and minor correction of the text.
ballarin
parents: 32983
diff changeset
    28
\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
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    29
\author{Clemens Ballarin}
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    30
\date{}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    31
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    32
\maketitle
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    33
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    34
\begin{abstract}
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    35
  Locales are Isabelle's approach for dealing with parametric
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    36
  theories.  They have been designed as a module system for a
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    37
  theorem prover that can adequately represent the complex
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    38
  inter-dependencies between structures found in abstract algebra, but
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    39
  have proven fruitful also in other applications --- for example,
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    40
  software verification.
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    41
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    42
  Both design and implementation of locales have evolved considerably
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    43
  since Kamm\"uller did his initial experiments.  Today, locales
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    44
  are a simple yet powerful extension of the Isar proof language.
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    45
  The present tutorial covers all major facilities of locales.  It is
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    46
  intended for locale novices; familiarity with Isabelle and Isar is
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    47
  presumed.
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    48
\end{abstract}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    49
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    50
\parindent 0pt\parskip 0.5ex
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    51
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    52
\input{session}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    53
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    54
\bibliographystyle{abbrv}
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    55
\bibliography{root}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    56
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    57
\end{document}
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    58
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    59
%%% Local Variables:
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    60
%%% mode: latex
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    61
%%% TeX-master: t
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    62
%%% End: