doc-src/Locales/Locales/document/root.tex
author wenzelm
Wed, 04 Jun 2008 17:12:00 +0200
changeset 27082 9102d87efd3d
parent 27078 41483ec1b5b6
child 29566 937baa077df2
permissions -rw-r--r--
tikz: change to pgfsys-dvi.def for plain dvi output;
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}
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     9
\usepackage{array}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    10
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    11
\usepackage{amssymb}
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    12
27078
41483ec1b5b6 work within *this* directory;
wenzelm
parents: 27068
diff changeset
    13
\usepackage{../../../pdfsetup}
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    14
27078
41483ec1b5b6 work within *this* directory;
wenzelm
parents: 27068
diff changeset
    15
\isadroptag{theory}
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    16
\isafoldtag{proof}
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    17
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    18
% urls in roman style, theory text in typewriter
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    19
\urlstyle{rm}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    20
\isabellestyle{tt}
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    21
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    22
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    23
\begin{document}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    24
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    25
\title{Tutorial to Locales and Locale Interpretation}
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    26
\author{Clemens Ballarin}
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    27
\date{}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    28
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    29
\maketitle
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    30
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    31
\thispagestyle{myheadings}
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    32
\markright{Technical Report TUM-I0723, Technische Universit\"at M\"unchen, 2007}
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    33
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    34
\begin{abstract}
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    35
  Locales are Isabelle's mechanism to deal with parametric theories.
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    36
  We present typical examples of locale specifications,
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    37
  along with interpretations between locales to change their
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    38
  hierarchic dependencies and interpretations to reuse locales in
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    39
  theory contexts and proofs.
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    40
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    41
  This tutorial is intended for locale novices; familiarity with
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    42
  Isabelle and Isar is presumed.
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    43
\end{abstract}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    44
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    45
\parindent 0pt\parskip 0.5ex
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    46
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    47
\input{session}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    48
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    49
\newpage
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    50
\bibliographystyle{abbrv}
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    51
\bibliography{root}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    52
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    53
\end{document}
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    54
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    55
%%% Local Variables:
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    56
%%% mode: latex
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    57
%%% TeX-master: t
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    58
%%% End: