doc-src/IsarRef/intro.tex
author haftmann
Fri Dec 29 12:11:04 2006 +0100 (2006-12-29)
changeset 21927 9677abe5d374
parent 21703 a9fdad55a53d
permissions -rw-r--r--
added handling for explicit classrel witnesses
wenzelm@7046
     1
wenzelm@7046
     2
\chapter{Introduction}
wenzelm@7046
     3
wenzelm@12618
     4
\section{Overview}
wenzelm@12618
     5
wenzelm@12618
     6
The \emph{Isabelle} system essentially provides a generic infrastructure for
wenzelm@12618
     7
building deductive systems (programmed in Standard ML), with a special focus
wenzelm@12618
     8
on interactive theorem proving in higher-order logics.  In the olden days even
wenzelm@12618
     9
end-users would refer to certain ML functions (goal commands, tactics,
wenzelm@12879
    10
tacticals etc.) to pursue their everyday theorem proving tasks
wenzelm@12618
    11
\cite{isabelle-intro,isabelle-ref}.
wenzelm@12618
    12
  
wenzelm@12618
    13
In contrast \emph{Isar} provides an interpreted language environment of its
wenzelm@12618
    14
own, which has been specifically tailored for the needs of theory and proof
wenzelm@12618
    15
development.  Compared to raw ML, the Isabelle/Isar top-level provides a more
wenzelm@12618
    16
robust and comfortable development platform, with proper support for theory
wenzelm@13039
    17
development graphs, single-step transactions with unlimited undo, etc.  The
wenzelm@12618
    18
Isabelle/Isar version of the \emph{Proof~General} user interface
wenzelm@12618
    19
\cite{proofgeneral,Aspinall:TACAS:2000} provides an adequate front-end for
wenzelm@13039
    20
interactive theory and proof development in this advanced theorem proving
wenzelm@13039
    21
environment.
wenzelm@12618
    22
wenzelm@13039
    23
\medskip Apart from the technical advances over bare-bones ML programming, the
wenzelm@13039
    24
main purpose of the Isar language is to provide a conceptually different view
wenzelm@13039
    25
on machine-checked proofs \cite{Wenzel:1999:TPHOL,Wenzel-PhD}.  ``Isar''
wenzelm@13039
    26
stands for ``Intelligible semi-automated reasoning''.  Drawing from both the
wenzelm@12618
    27
traditions of informal mathematical proof texts and high-level programming
wenzelm@13039
    28
languages, Isar offers a versatile environment for structured formal proof
wenzelm@13039
    29
documents.  Thus properly written Isar proofs become accessible to a broader
wenzelm@13039
    30
audience than unstructured tactic scripts (which typically only provide
wenzelm@13039
    31
operational information for the machine).  Writing human-readable proof texts
wenzelm@13039
    32
certainly requires some additional efforts by the writer to achieve a good
wenzelm@13039
    33
presentation, both of formal and informal parts of the text.  On the other
wenzelm@13039
    34
hand, human-readable formal texts gain some value in their own right,
wenzelm@13039
    35
independently of the mechanic proof-checking process.
wenzelm@12618
    36
wenzelm@12618
    37
Despite its grand design of structured proof texts, Isar is able to assimilate
wenzelm@12879
    38
the old tactical style as an ``improper'' sub-language.  This provides an easy
wenzelm@12618
    39
upgrade path for existing tactic scripts, as well as additional means for
wenzelm@12879
    40
interactive experimentation and debugging of structured proofs.  Isabelle/Isar
wenzelm@12879
    41
supports a broad range of proof styles, both readable and unreadable ones.
wenzelm@12618
    42
wenzelm@12879
    43
\medskip The Isabelle/Isar framework is generic and should work reasonably
wenzelm@12879
    44
well for any Isabelle object-logic that conforms to the natural deduction view
wenzelm@12879
    45
of the Isabelle/Pure framework.  Major Isabelle logics like HOL
wenzelm@12879
    46
\cite{isabelle-HOL}, HOLCF \cite{MuellerNvOS99}, FOL \cite{isabelle-logics},
wenzelm@12879
    47
and ZF \cite{isabelle-ZF} have already been set up for end-users.
wenzelm@12879
    48
Nonetheless, much of the existing body of theories still consist of old-style
wenzelm@12879
    49
theory files with accompanied ML code for proof scripts; this legacy will be
wenzelm@12879
    50
gradually converted in due time.
wenzelm@12618
    51
wenzelm@12618
    52
wenzelm@7167
    53
\section{Quick start}
wenzelm@7167
    54
wenzelm@8508
    55
\subsection{Terminal sessions}
wenzelm@8508
    56
wenzelm@12879
    57
Isar is already part of Isabelle.  The low-level \texttt{isabelle} binary
wenzelm@12879
    58
provides option \texttt{-I} to run the Isabelle/Isar interaction loop at
wenzelm@12879
    59
startup, rather than the raw ML top-level.  So the most basic way to do
wenzelm@12879
    60
anything with Isabelle/Isar is as follows:
wenzelm@7175
    61
\begin{ttbox}
wenzelm@7175
    62
isabelle -I HOL\medskip
wenzelm@17567
    63
\out{> Welcome to Isabelle/HOL (Isabelle2005)}\medskip
wenzelm@17567
    64
theory Foo imports Main begin;
wenzelm@7297
    65
constdefs foo :: nat  "foo == 1";
wenzelm@7297
    66
lemma "0 < foo" by (simp add: foo_def);
wenzelm@17567
    67
end;
wenzelm@7175
    68
\end{ttbox}
wenzelm@9233
    69
Note that any Isabelle/Isar command may be retracted by \texttt{undo}.  See
wenzelm@10160
    70
the Isabelle/Isar Quick Reference (appendix~\ref{ap:refcard}) for a
wenzelm@10110
    71
comprehensive overview of available commands and other language elements.
wenzelm@7175
    72
wenzelm@8508
    73
wenzelm@8843
    74
\subsection{Proof~General}
wenzelm@8508
    75
wenzelm@8508
    76
Plain TTY-based interaction as above used to be quite feasible with
wenzelm@8547
    77
traditional tactic based theorem proving, but developing Isar documents really
wenzelm@12879
    78
demands some better user-interface support.  The Proof~General environment by
wenzelm@12879
    79
David Aspinall \cite{proofgeneral,Aspinall:TACAS:2000} offers a generic Emacs
wenzelm@12879
    80
interface for interactive theorem provers that organizes all the cut-and-paste
wenzelm@12879
    81
and forward-backward walk through the text in a very neat way.  In
wenzelm@12879
    82
Isabelle/Isar, the current position within a partial proof document is equally
wenzelm@12879
    83
important than the actual proof state.  Thus Proof~General provides the
wenzelm@12879
    84
canonical working environment for Isabelle/Isar, both for getting acquainted
wenzelm@12879
    85
(e.g.\ by replaying existing Isar documents) and for production work.
wenzelm@7175
    86
wenzelm@8843
    87
wenzelm@8843
    88
\subsubsection{Proof~General as default Isabelle interface}
wenzelm@7167
    89
wenzelm@12879
    90
The Isabelle interface wrapper script provides an easy way to invoke
wenzelm@21703
    91
Proof~General (including XEmacs or GNU Emacs).  The default
wenzelm@21703
    92
configuration of Isabelle is smart enough to detect the Proof~General
wenzelm@21703
    93
distribution in several canonical places (e.g.\ 
wenzelm@21703
    94
\texttt{\$ISABELLE_HOME/contrib/ProofGeneral}).  Thus the capital
wenzelm@21703
    95
\texttt{Isabelle} executable would already refer to the
wenzelm@21703
    96
\texttt{ProofGeneral/isar} interface without further ado.  The
wenzelm@21703
    97
Isabelle interface script provides several options; pass \verb,-?, to
wenzelm@21703
    98
see its usage.
wenzelm@7981
    99
wenzelm@7175
   100
With the proper Isabelle interface setup, Isar documents may now be edited by
wenzelm@7175
   101
visiting appropriate theory files, e.g.\ 
wenzelm@7175
   102
\begin{ttbox}
wenzelm@12879
   103
Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/Summation.thy
wenzelm@7175
   104
\end{ttbox}
wenzelm@13039
   105
Beginners may note the tool bar for navigating forward and backward through
wenzelm@13039
   106
the text (this depends on the local Emacs installation).  Consult the
wenzelm@12879
   107
Proof~General documentation \cite{proofgeneral} for further basic command
wenzelm@12879
   108
sequences, in particular ``\texttt{C-c C-return}'' and ``\texttt{C-c u}''.
wenzelm@8508
   109
wenzelm@9849
   110
\medskip
wenzelm@9849
   111
wenzelm@9849
   112
Proof~General may be also configured manually by giving Isabelle settings like
wenzelm@9849
   113
this (see also \cite{isabelle-sys}):
wenzelm@9849
   114
\begin{ttbox}
wenzelm@9849
   115
ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
wenzelm@9849
   116
PROOFGENERAL_OPTIONS=""
wenzelm@9849
   117
\end{ttbox}
wenzelm@9849
   118
You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the
wenzelm@9849
   119
actual installation directory of Proof~General.
wenzelm@9849
   120
wenzelm@9849
   121
\medskip
wenzelm@9849
   122
wenzelm@9849
   123
Apart from the Isabelle command line, defaults for interface options may be
wenzelm@12879
   124
given by the \texttt{PROOFGENERAL_OPTIONS} setting.  For example, the Emacs
wenzelm@12879
   125
executable to be used may be configured in Isabelle's settings like this:
wenzelm@9849
   126
\begin{ttbox}
wenzelm@16016
   127
PROOFGENERAL_OPTIONS="-p xemacs-mule"  
wenzelm@9849
   128
\end{ttbox}
wenzelm@9849
   129
wenzelm@12879
   130
Occasionally, a user's \verb,~/.emacs, file contains code that is incompatible
wenzelm@12879
   131
with the (X)Emacs version used by Proof~General, causing the interface startup
wenzelm@12879
   132
to fail prematurely.  Here the \texttt{-u false} option helps to get the
wenzelm@12879
   133
interface process up and running.  Note that additional Lisp customization
wenzelm@12879
   134
code may reside in \texttt{proofgeneral-settings.el} of
wenzelm@12879
   135
\texttt{\$ISABELLE_HOME/etc} or \texttt{\$ISABELLE_HOME_USER/etc}.
wenzelm@9849
   136
wenzelm@8843
   137
wenzelm@8843
   138
\subsubsection{The X-Symbol package}
wenzelm@8508
   139
wenzelm@12879
   140
Proof~General provides native support for the Emacs X-Symbol package
wenzelm@12879
   141
\cite{x-symbol}, which handles proper mathematical symbols displayed on
wenzelm@12879
   142
screen.  Pass option \texttt{-x true} to the Isabelle interface script, or
wenzelm@12879
   143
check the appropriate Proof~General menu setting by hand.  In any case, the
wenzelm@12879
   144
X-Symbol package must have been properly installed already.
wenzelm@8516
   145
wenzelm@8843
   146
Contrary to what you may expect from the documentation of X-Symbol, the
wenzelm@9849
   147
package is very easy to install and configures itself automatically.  The
wenzelm@9849
   148
default configuration of Isabelle is smart enough to detect the X-Symbol
wenzelm@9849
   149
package in several canonical places (e.g.\ 
wenzelm@9849
   150
\texttt{\$ISABELLE_HOME/contrib/x-symbol}).
wenzelm@8843
   151
wenzelm@8843
   152
\medskip
wenzelm@8843
   153
wenzelm@8843
   154
Using proper mathematical symbols in Isabelle theories can be very convenient
wenzelm@8843
   155
for readability of large formulas.  On the other hand, the plain ASCII sources
wenzelm@10160
   156
easily become somewhat unintelligible.  For example, $\Longrightarrow$ would
wenzelm@9849
   157
appear as \verb,\<Longrightarrow>, according the default set of Isabelle
wenzelm@9849
   158
symbols.  Nevertheless, the Isabelle document preparation system (see
wenzelm@9849
   159
\S\ref{sec:document-prep}) will be happy to print non-ASCII symbols properly.
wenzelm@9849
   160
It is even possible to invent additional notation beyond the display
wenzelm@12879
   161
capabilities of Emacs and X-Symbol.
wenzelm@7175
   162
wenzelm@7981
   163
wenzelm@7981
   164
\section{Isabelle/Isar theories}
wenzelm@7981
   165
wenzelm@8547
   166
Isabelle/Isar offers the following main improvements over classic Isabelle.
wenzelm@7981
   167
\begin{enumerate}
wenzelm@13039
   168
  
wenzelm@7981
   169
\item A new \emph{theory format}, occasionally referred to as ``new-style
wenzelm@7981
   170
  theories'', supporting interactive development and unlimited undo operation.
wenzelm@13039
   171
  
wenzelm@7981
   172
\item A \emph{formal proof document language} designed to support intelligible
wenzelm@7981
   173
  semi-automated reasoning.  Instead of putting together unreadable tactic
wenzelm@7981
   174
  scripts, the author is enabled to express the reasoning in way that is close
wenzelm@13039
   175
  to usual mathematical practice.  The old tactical style has been assimilated
wenzelm@13039
   176
  as ``improper'' language elements.
wenzelm@13039
   177
  
wenzelm@8547
   178
\item A simple document preparation system, for typesetting formal
wenzelm@8547
   179
  developments together with informal text.  The resulting hyper-linked PDF
wenzelm@8547
   180
  documents are equally well suited for WWW presentation and as printed
wenzelm@8547
   181
  copies.
wenzelm@13039
   182
wenzelm@7981
   183
\end{enumerate}
wenzelm@7981
   184
wenzelm@7981
   185
The Isar proof language is embedded into the new theory format as a proper
wenzelm@7981
   186
sub-language.  Proof mode is entered by stating some $\THEOREMNAME$ or
wenzelm@7981
   187
$\LEMMANAME$ at the theory level, and left again with the final conclusion
wenzelm@12879
   188
(e.g.\ via $\QEDNAME$).  A few theory specification mechanisms also require
wenzelm@12879
   189
some proof, such as HOL's $\isarkeyword{typedef}$ which demands non-emptiness
wenzelm@12879
   190
of the representing sets.
wenzelm@7460
   191
wenzelm@7981
   192
New-style theory files may still be associated with separate ML files
wenzelm@7981
   193
consisting of plain old tactic scripts.  There is no longer any ML binding
wenzelm@7981
   194
generated for the theory and theorems, though.  ML functions \texttt{theory},
wenzelm@13039
   195
\texttt{thm}, and \texttt{thms} retrieve this information from the context
wenzelm@13039
   196
\cite{isabelle-ref}.  Nevertheless, migration between classic Isabelle and
wenzelm@13039
   197
Isabelle/Isar is relatively easy.  Thus users may start to benefit from
wenzelm@13039
   198
interactive theory development and document preparation, even before they have
wenzelm@13039
   199
any idea of the Isar proof language at all.
wenzelm@7981
   200
wenzelm@7981
   201
\begin{warn}
wenzelm@12879
   202
  Proof~General does \emph{not} support mixed interactive development of
wenzelm@12879
   203
  classic Isabelle theory files or tactic scripts, together with Isar
wenzelm@12879
   204
  documents.  The ``\texttt{isa}'' and ``\texttt{isar}'' versions of
wenzelm@7981
   205
  Proof~General are handled as two different theorem proving systems, only one
wenzelm@7981
   206
  of these may be active at the same time.
wenzelm@7981
   207
\end{warn}
wenzelm@7981
   208
wenzelm@12879
   209
Manual conversion of existing tactic scripts may be done by running two
wenzelm@12879
   210
separate Proof~General sessions, one for replaying the old script and the
wenzelm@12879
   211
other for the emerging Isabelle/Isar document.  Also note that Isar supports
wenzelm@12879
   212
emulation commands and methods that support traditional tactic scripts within
wenzelm@12879
   213
new-style theories, see appendix~\ref{ap:conv} for more information.
wenzelm@7981
   214
wenzelm@7167
   215
wenzelm@8843
   216
\subsection{Document preparation}\label{sec:document-prep}
wenzelm@8684
   217
wenzelm@12879
   218
Isabelle/Isar provides a simple document preparation system based on existing
wenzelm@13039
   219
{PDF-\LaTeX} technology, with full support of hyper-links (both local
wenzelm@13039
   220
references and URLs), bookmarks, and thumbnails.  Thus the results are equally
wenzelm@13039
   221
well suited for WWW browsing and as printed copies.
wenzelm@8684
   222
wenzelm@8684
   223
\medskip
wenzelm@8684
   224
wenzelm@8684
   225
Isabelle generates {\LaTeX} output as part of the run of a \emph{logic
wenzelm@8684
   226
  session} (see also \cite{isabelle-sys}).  Getting started with a working
wenzelm@8684
   227
configuration for common situations is quite easy by using the Isabelle
wenzelm@12879
   228
\texttt{mkdir} and \texttt{make} tools.  First invoke
wenzelm@8684
   229
\begin{ttbox}
wenzelm@12879
   230
  isatool mkdir Foo
wenzelm@8684
   231
\end{ttbox}
wenzelm@12879
   232
to initialize a separate directory for session \texttt{Foo} --- it is safe to
wenzelm@12879
   233
experiment, since \texttt{isatool mkdir} never overwrites existing files.
wenzelm@12879
   234
Ensure that \texttt{Foo/ROOT.ML} holds ML commands to load all theories
wenzelm@12879
   235
required for this session; furthermore \texttt{Foo/document/root.tex} should
wenzelm@12879
   236
include any special {\LaTeX} macro packages required for your document (the
wenzelm@12879
   237
default is usually sufficient as a start).
wenzelm@8684
   238
wenzelm@12879
   239
The session is controlled by a separate \texttt{IsaMakefile} (with crude
wenzelm@12879
   240
source dependencies by default).  This file is located one level up from the
wenzelm@12879
   241
\texttt{Foo} directory location.  Now invoke
wenzelm@8684
   242
\begin{ttbox}
wenzelm@8684
   243
  isatool make Foo
wenzelm@8684
   244
\end{ttbox}
wenzelm@8684
   245
to run the \texttt{Foo} session, with browser information and document
wenzelm@8684
   246
preparation enabled.  Unless any errors are reported by Isabelle or {\LaTeX},
wenzelm@12879
   247
the output will appear inside the directory \texttt{ISABELLE_BROWSER_INFO}, as
wenzelm@12879
   248
reported by the batch job in verbose mode.
wenzelm@8684
   249
wenzelm@8684
   250
\medskip
wenzelm@8684
   251
wenzelm@8684
   252
You may also consider to tune the \texttt{usedir} options in
wenzelm@8684
   253
\texttt{IsaMakefile}, for example to change the output format from
wenzelm@13039
   254
\texttt{pdf} to \texttt{dvi}, or activate the \texttt{-D} option to retain a
wenzelm@13039
   255
second copy of the generated {\LaTeX} sources.
wenzelm@8684
   256
wenzelm@8684
   257
\medskip
wenzelm@8684
   258
wenzelm@8684
   259
See \emph{The Isabelle System Manual} \cite{isabelle-sys} for further details
wenzelm@12879
   260
on Isabelle logic sessions and theory presentation.  The Isabelle/HOL tutorial
wenzelm@12879
   261
\cite{isabelle-hol-book} also covers theory presentation issues.
wenzelm@8684
   262
wenzelm@8684
   263
wenzelm@10160
   264
\subsection{How to write Isar proofs anyway?}\label{sec:isar-howto}
wenzelm@7167
   265
wenzelm@12879
   266
This is one of the key questions, of course.  First of all, the tactic script
wenzelm@12879
   267
emulation of Isabelle/Isar essentially provides a clarified version of the
wenzelm@12879
   268
very same unstructured proof style of classic Isabelle.  Old-time users should
wenzelm@13039
   269
quickly become acquainted with that (slightly degenerative) view of Isar.
wenzelm@12621
   270
wenzelm@12879
   271
Writing \emph{proper} Isar proof texts targeted at human readers is quite
wenzelm@12879
   272
different, though.  Experienced users of the unstructured style may even have
wenzelm@12879
   273
to unlearn some of their habits to master proof composition in Isar.  In
wenzelm@12879
   274
contrast, new users with less experience in old-style tactical proving, but a
wenzelm@13039
   275
good understanding of mathematical proof in general, often get started easier.
wenzelm@7297
   276
wenzelm@12879
   277
\medskip The present text really is only a reference manual on Isabelle/Isar,
wenzelm@12879
   278
not a tutorial.  Nevertheless, we will attempt to give some clues of how the
wenzelm@12879
   279
concepts introduced here may be put into practice.  Appendix~\ref{ap:refcard}
wenzelm@12879
   280
provides a quick reference card of the most common Isabelle/Isar language
wenzelm@12879
   281
elements.  Appendix~\ref{ap:conv} offers some practical hints on converting
wenzelm@12879
   282
existing Isabelle theories and proof scripts to the new format (without
wenzelm@12879
   283
restructuring proofs).
wenzelm@10160
   284
wenzelm@12879
   285
Further issues concerning the Isar concepts are covered in the literature
wenzelm@12879
   286
\cite{Wenzel:1999:TPHOL,Wiedijk:2000:MV,Bauer-Wenzel:2000:HB,Bauer-Wenzel:2001}.
wenzelm@12879
   287
The author's PhD thesis \cite{Wenzel-PhD} presently provides the most complete
wenzelm@12879
   288
exposition of Isar foundations, techniques, and applications.  A number of
wenzelm@12879
   289
example applications are distributed with Isabelle, and available via the
wenzelm@12879
   290
Isabelle WWW library (e.g.\ \url{http://isabelle.in.tum.de/library/}).  As a
wenzelm@12879
   291
general rule of thumb, more recent Isabelle applications that also include a
wenzelm@12879
   292
separate ``document'' (in PDF) are more likely to consist of proper
wenzelm@12879
   293
Isabelle/Isar theories and proofs.
wenzelm@7836
   294
wenzelm@12879
   295
%FIXME
wenzelm@12879
   296
% The following examples may be of particular interest.  Apart from the plain
wenzelm@12879
   297
% sources represented in HTML, these Isabelle sessions also provide actual
wenzelm@12879
   298
% documents (in PDF).
wenzelm@12879
   299
% \begin{itemize}
wenzelm@12879
   300
% \item \url{http://isabelle.in.tum.de/library/HOL/Isar_examples/} is a
wenzelm@12879
   301
%   collection of introductory examples.
wenzelm@12879
   302
% \item \url{http://isabelle.in.tum.de/library/HOL/Lattice/} is an example of
wenzelm@12879
   303
%   typical mathematics-style reasoning in ``axiomatic'' structures.
wenzelm@12879
   304
% \item \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/HahnBanach/} is a
wenzelm@12879
   305
%   big mathematics application on infinitary vector spaces and functional
wenzelm@12879
   306
%   analysis.
wenzelm@12879
   307
% \item \url{http://isabelle.in.tum.de/library/HOL/Lambda/} develops fundamental
wenzelm@12879
   308
%   properties of $\lambda$-calculus (Church-Rosser and termination).
wenzelm@10993
   309
  
wenzelm@12879
   310
%   This may serve as a realistic example of porting of legacy proof scripts
wenzelm@12879
   311
%   into Isar tactic emulation scripts.
wenzelm@12879
   312
% \item \url{http://isabelle.in.tum.de/library/HOL/Unix/} gives a mathematical
wenzelm@12879
   313
%   model of the main aspects of the Unix file-system including its security
wenzelm@12879
   314
%   model, but ignoring processes.  A few odd effects caused by the general
wenzelm@12879
   315
%   ``worse-is-better'' approach followed in Unix are discussed within the
wenzelm@12879
   316
%   formal model.
wenzelm@10993
   317
  
wenzelm@12879
   318
%   This example represents a non-trivial verification task, with all proofs
wenzelm@12879
   319
%   carefully worked out using the proper part of the Isar proof language;
wenzelm@12879
   320
%   unstructured scripts are only used for symbolic evaluation.
wenzelm@12879
   321
% \item \url{http://isabelle.in.tum.de/library/HOL/MicroJava/} is a
wenzelm@12879
   322
%   formalization of a fragment of Java, together with a corresponding virtual
wenzelm@12879
   323
%   machine and a specification of its bytecode verifier and a lightweight
wenzelm@12879
   324
%   bytecode verifier, including proofs of type-safety.
wenzelm@10993
   325
  
wenzelm@12879
   326
%   This represents a very ``realistic'' example of large formalizations
wenzelm@12879
   327
%   performed in form of tactic emulation scripts and proper Isar proof texts.
wenzelm@12879
   328
% \end{itemize}
wenzelm@8547
   329
wenzelm@7167
   330
wenzelm@7046
   331
%%% Local Variables: 
wenzelm@7046
   332
%%% mode: latex
wenzelm@7046
   333
%%% TeX-master: "isar-ref"
wenzelm@7046
   334
%%% End: