doc-src/Locales/Locales/document/root.tex
author ballarin
Tue, 03 Jun 2008 12:34:22 +0200
changeset 27063 d1d35284542f
parent 26911 871cc7f11034
child 27068 c63875c75fbf
permissions -rw-r--r--
New version covering interpretation.
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}
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
     3
\usepackage{tikz}
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
     4
\usepackage{subfigure}
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
     5
\usepackage{isabelle,isabellesym}
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
     6
\usepackage{verbatim}
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     7
\usepackage{array}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     8
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
     9
% further packages required for unusual symbols (see also
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    10
% isabellesym.sty), use only when needed
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    11
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    12
\usepackage{amssymb}
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    13
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    14
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    15
  %\<triangleq>, \<yen>, \<lozenge>
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    16
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    17
%\usepackage[greek,english]{babel}
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    18
  %option greek for \<euro>
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    19
  %option english (default language) for \<guillemotleft>, \<guillemotright>
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    20
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    21
%\usepackage[latin1]{inputenc}
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    22
  %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    23
  %\<threesuperior>, \<threequarters>, \<degree>
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    24
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    25
%\usepackage[only,bigsqcap]{stmaryrd}
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    26
  %for \<Sqinter>
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    27
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    28
%\usepackage{eufrak}
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    29
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    30
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    31
%\usepackage{textcomp}
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    32
  %for \<cent>, \<currency>
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    33
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    34
% this should be the last package used
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    35
\usepackage{pdfsetup}
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    36
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    37
\isafoldtag{proof}
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    38
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    39
% urls in roman style, theory text in typewriter
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    40
\urlstyle{rm}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    41
\isabellestyle{tt}
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    42
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    43
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    44
\begin{document}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    45
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    46
\title{Tutorial to Locales and Locale Interpretation}
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    47
\author{Clemens Ballarin}
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    48
\date{}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    49
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    50
\maketitle
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    51
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    52
\thispagestyle{myheadings}
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    53
\markright{Technical Report TUM-I0723, Technische Universit\"at M\"unchen, 2007}
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    54
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    55
\begin{abstract}
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    56
  Locales are Isabelle's mechanism to deal with parametric theories.
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    57
  We present typical examples of locale specifications,
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    58
  along with interpretations between locales to change their
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    59
  hierarchic dependencies and interpretations to reuse locales in
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    60
  theory contexts and proofs.
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    61
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    62
  This tutorial is intended for locale novices; familiarity with
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    63
  Isabelle and Isar is presumed.
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    64
\end{abstract}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    65
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    66
\parindent 0pt\parskip 0.5ex
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    67
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    68
% generated text of all theories
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    69
\input{session}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    70
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    71
% optional bibliography
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    72
\newpage
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    73
\bibliographystyle{abbrv}
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    74
\bibliography{root}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    75
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    76
\end{document}
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    77
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    78
%%% Local Variables:
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    79
%%% mode: latex
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    80
%%% TeX-master: t
d1d35284542f New version covering interpretation.
ballarin
parents: 26911
diff changeset
    81
%%% End: