doc-src/Locales/Locales/document/root.tex
author ballarin
Fri, 16 Apr 2004 11:35:44 +0200
changeset 14586 7b8d56b4ac60
child 26911 871cc7f11034
permissions -rw-r--r--
Added Locales Tutorial.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     1
\documentclass[leqno]{article}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     2
\usepackage{isabelle,isabellesym}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     3
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     4
\usepackage{amsmath}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     5
\usepackage{amssymb}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     6
\usepackage{array}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     7
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     8
% this should be the last package used
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     9
\usepackage{pdfsetup}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    10
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    11
\urlstyle{rm}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    12
\isabellestyle{tt}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    13
%\renewcommand{\isacharunderscore}{\_}%
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    14
% the latter is not necessary with \isabellestyle{tt}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    15
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    16
\begin{document}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    17
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    18
\title{Locales and Locale Expressions in Isabelle/Isar}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    19
\author{Clemens Ballarin \\
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    20
  Fakult\"at f\"ur Informatik \\ Technische Universit\"at M\"unchen \\
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    21
  85748 Garching, Germany \\
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    22
  ballarin@in.tum.de}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    23
\date{}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    24
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    25
\maketitle
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    26
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    27
\begin{abstract}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    28
  Locales provide a module system for the Isabelle proof assistant.
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    29
  Recently, locales have been ported to the new Isar format for
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    30
  structured proofs.  At the same time, they have been extended by
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    31
  locale expressions, a language for composing locale specifications,
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    32
  and by structures, which provide syntax for algebraic structures.
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    33
  The present paper presents both and is suitable as a tutorial to
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    34
  locales in Isar, because it covers both basics and recent
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    35
  extensions, and contains many examples.
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    36
\end{abstract}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    37
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    38
%\tableofcontents
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    39
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    40
\parindent 0pt\parskip 0.5ex
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    41
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    42
% include generated text of all theories
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    43
\input{session}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    44
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    45
\bibliographystyle{plain}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    46
\bibliography{root}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    47
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    48
\end{document}