doc-src/TutorialI/basics.tex
author nipkow
Mon Mar 19 12:38:36 2001 +0100 (2001-03-19)
changeset 11213 aeb5c72dd72a
parent 11209 a8cb33f6cf9c
child 11301 be4163219703
permissions -rw-r--r--
*** empty log message ***
nipkow@8743
     1
\chapter{Basic Concepts}
nipkow@8743
     2
nipkow@8743
     3
\section{Introduction}
nipkow@8743
     4
nipkow@10971
     5
This is a tutorial on how to use the theorem prover Isabelle/HOL as a specification and
nipkow@8743
     6
verification system. Isabelle is a generic system for implementing logical
nipkow@8743
     7
formalisms, and Isabelle/HOL is the specialization of Isabelle for
nipkow@8743
     8
HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step
nipkow@8743
     9
following the equation
nipkow@8743
    10
\[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]
nipkow@10983
    11
We do not assume that the reader is familiar with mathematical logic but that
nipkow@11209
    12
(s)he is used to logical and set theoretic notation, such as covered
nipkow@11209
    13
in a good discrete math course~\cite{Rosen-DMA}. In contrast, we do assume
nipkow@11209
    14
that the reader is familiar with the basic concepts of functional
nipkow@11209
    15
programming~\cite{Bird-Haskell,Hudak-Haskell,paulson-ml2,Thompson-Haskell}.
nipkow@11209
    16
Although this tutorial initially concentrates on functional programming, do
nipkow@11209
    17
not be misled: HOL can express most mathematical concepts, and functional
nipkow@11209
    18
programming is just one particularly simple and ubiquitous instance.
nipkow@8743
    19
nipkow@11205
    20
Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}.  This has
nipkow@11205
    21
influenced some of Isabelle/HOL's concrete syntax but is otherwise irrelevant
nipkow@11205
    22
for us because this tutorial is based on
nipkow@11213
    23
Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle which hides
nipkow@11213
    24
the implementation language almost completely.  Thus the full name of the
nipkow@11213
    25
system should be Isabelle/Isar/HOL, but that is a bit of a mouthful.
nipkow@11213
    26
nipkow@11213
    27
There are other implementations of HOL, in particular the one by Mike Gordon
nipkow@11213
    28
\emph{et al.}, which is usually referred to as ``the HOL system''
nipkow@11213
    29
\cite{mgordon-hol}. For us, HOL refers to the logical system, and sometimes
nipkow@11213
    30
its incarnation Isabelle/HOL.
nipkow@8743
    31
nipkow@8743
    32
A tutorial is by definition incomplete.  Currently the tutorial only
nipkow@8743
    33
introduces the rudiments of Isar's proof language. To fully exploit the power
nipkow@11213
    34
of Isar, in particular the ability to write readable and structured proofs,
nipkow@11213
    35
you need to consult the Isabelle/Isar Reference
nipkow@8743
    36
Manual~\cite{isabelle-isar-ref}. If you want to use Isabelle's ML level
nipkow@8743
    37
directly (for example for writing your own proof procedures) see the Isabelle
nipkow@8743
    38
Reference Manual~\cite{isabelle-ref}; for details relating to HOL see the
nipkow@8743
    39
Isabelle/HOL manual~\cite{isabelle-HOL}. All manuals have a comprehensive
nipkow@8743
    40
index.
nipkow@8743
    41
nipkow@8743
    42
\section{Theories}
nipkow@8743
    43
\label{sec:Basic:Theories}
nipkow@8743
    44
nipkow@8743
    45
Working with Isabelle means creating theories. Roughly speaking, a
nipkow@8743
    46
\bfindex{theory} is a named collection of types, functions, and theorems,
nipkow@8743
    47
much like a module in a programming language or a specification in a
nipkow@8743
    48
specification language. In fact, theories in HOL can be either. The general
nipkow@8743
    49
format of a theory \texttt{T} is
nipkow@8743
    50
\begin{ttbox}
nipkow@8743
    51
theory T = B\(@1\) + \(\cdots\) + B\(@n\):
nipkow@8743
    52
\(\textit{declarations, definitions, and proofs}\)
nipkow@8743
    53
end
nipkow@8743
    54
\end{ttbox}
nipkow@8743
    55
where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing
nipkow@8743
    56
theories that \texttt{T} is based on and \texttt{\textit{declarations,
nipkow@8743
    57
    definitions, and proofs}} represents the newly introduced concepts
nipkow@8771
    58
(types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the
nipkow@8743
    59
direct \textbf{parent theories}\indexbold{parent theory} of \texttt{T}.
nipkow@8743
    60
Everything defined in the parent theories (and their parents \dots) is
nipkow@8743
    61
automatically visible. To avoid name clashes, identifiers can be
nipkow@8743
    62
\textbf{qualified} by theory names as in \texttt{T.f} and
nipkow@8743
    63
\texttt{B.f}.\indexbold{identifier!qualified} Each theory \texttt{T} must
nipkow@8771
    64
reside in a \bfindex{theory file} named \texttt{T.thy}.
nipkow@8743
    65
nipkow@8743
    66
This tutorial is concerned with introducing you to the different linguistic
nipkow@8743
    67
constructs that can fill \textit{\texttt{declarations, definitions, and
nipkow@8743
    68
    proofs}} in the above theory template.  A complete grammar of the basic
nipkow@8743
    69
constructs is found in the Isabelle/Isar Reference Manual.
nipkow@8743
    70
paulson@10885
    71
HOL's theory collection is available online at
nipkow@8743
    72
\begin{center}\small
nipkow@10978
    73
    \url{http://isabelle.in.tum.de/library/HOL/}
nipkow@8743
    74
\end{center}
paulson@10885
    75
and is recommended browsing. Note that most of the theories 
nipkow@9541
    76
are based on classical Isabelle without the Isar extension. This means that
nipkow@9541
    77
they look slightly different than the theories in this tutorial, and that all
nipkow@9541
    78
proofs are in separate ML files.
nipkow@9541
    79
nipkow@8743
    80
\begin{warn}
nipkow@9792
    81
  HOL contains a theory \isaindexbold{Main}, the union of all the basic
paulson@10885
    82
  predefined theories like arithmetic, lists, sets, etc.  
paulson@10885
    83
  Unless you know what you are doing, always include \isa{Main}
nipkow@10971
    84
  as a direct or indirect parent of all your theories.
nipkow@8743
    85
\end{warn}
nipkow@8743
    86
nipkow@8743
    87
paulson@10885
    88
\section{Types, Terms and Formulae}
nipkow@8743
    89
\label{sec:TypesTermsForms}
nipkow@8743
    90
\indexbold{type}
nipkow@8743
    91
paulson@10795
    92
Embedded in a theory are the types, terms and formulae of HOL\@. HOL is a typed
nipkow@8771
    93
logic whose type system resembles that of functional programming languages
nipkow@8771
    94
like ML or Haskell. Thus there are
nipkow@8743
    95
\begin{description}
nipkow@8771
    96
\item[base types,] in particular \isaindex{bool}, the type of truth values,
nipkow@8771
    97
and \isaindex{nat}, the type of natural numbers.
nipkow@8771
    98
\item[type constructors,] in particular \isaindex{list}, the type of
nipkow@8771
    99
lists, and \isaindex{set}, the type of sets. Type constructors are written
nipkow@8771
   100
postfix, e.g.\ \isa{(nat)list} is the type of lists whose elements are
nipkow@8743
   101
natural numbers. Parentheses around single arguments can be dropped (as in
nipkow@8771
   102
\isa{nat list}), multiple arguments are separated by commas (as in
nipkow@8771
   103
\isa{(bool,nat)ty}).
nipkow@8743
   104
\item[function types,] denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}.
nipkow@8771
   105
  In HOL \isasymFun\ represents \emph{total} functions only. As is customary,
nipkow@8771
   106
  \isa{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means
nipkow@8771
   107
  \isa{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also
nipkow@8771
   108
  supports the notation \isa{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}
nipkow@8771
   109
  which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
nipkow@8743
   110
    \isasymFun~$\tau$}.
nipkow@8771
   111
\item[type variables,]\indexbold{type variable}\indexbold{variable!type}
paulson@10795
   112
  denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML\@. They give rise
nipkow@8771
   113
  to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity
nipkow@8771
   114
  function.
nipkow@8743
   115
\end{description}
nipkow@8743
   116
\begin{warn}
nipkow@8743
   117
  Types are extremely important because they prevent us from writing
nipkow@8743
   118
  nonsense.  Isabelle insists that all terms and formulae must be well-typed
nipkow@8743
   119
  and will print an error message if a type mismatch is encountered. To
nipkow@8743
   120
  reduce the amount of explicit type information that needs to be provided by
nipkow@8743
   121
  the user, Isabelle infers the type of all variables automatically (this is
nipkow@8743
   122
  called \bfindex{type inference}) and keeps quiet about it. Occasionally
nipkow@8743
   123
  this may lead to misunderstandings between you and the system. If anything
nipkow@8743
   124
  strange happens, we recommend to set the \rmindex{flag}
nipkow@9792
   125
  \isaindexbold{show_types} that tells Isabelle to display type information
nipkow@8743
   126
  that is usually suppressed: simply type
nipkow@8743
   127
\begin{ttbox}
nipkow@8743
   128
ML "set show_types"
nipkow@8743
   129
\end{ttbox}
nipkow@8743
   130
nipkow@8743
   131
\noindent
nipkow@10971
   132
This can be reversed by \texttt{ML "reset show_types"}. Various other flags,
nipkow@10971
   133
which we introduce as we go along,
nipkow@8771
   134
can be set and reset in the same manner.\indexbold{flag!(re)setting}
nipkow@8743
   135
\end{warn}
nipkow@8743
   136
nipkow@8743
   137
nipkow@8743
   138
\textbf{Terms}\indexbold{term} are formed as in functional programming by
nipkow@8771
   139
applying functions to arguments. If \isa{f} is a function of type
nipkow@8771
   140
\isa{$\tau@1$ \isasymFun~$\tau@2$} and \isa{t} is a term of type
nipkow@8771
   141
$\tau@1$ then \isa{f~t} is a term of type $\tau@2$. HOL also supports
nipkow@8771
   142
infix functions like \isa{+} and some basic constructs from functional
nipkow@8743
   143
programming:
nipkow@8743
   144
\begin{description}
nipkow@8771
   145
\item[\isa{if $b$ then $t@1$ else $t@2$}]\indexbold{*if}
nipkow@8743
   146
means what you think it means and requires that
nipkow@8771
   147
$b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type.
nipkow@8771
   148
\item[\isa{let $x$ = $t$ in $u$}]\indexbold{*let}
nipkow@8743
   149
is equivalent to $u$ where all occurrences of $x$ have been replaced by
nipkow@8743
   150
$t$. For example,
nipkow@8771
   151
\isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated
nipkow@8771
   152
by semicolons: \isa{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}.
nipkow@8771
   153
\item[\isa{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
nipkow@8743
   154
\indexbold{*case}
nipkow@8771
   155
evaluates to $e@i$ if $e$ is of the form $c@i$.
nipkow@8743
   156
\end{description}
nipkow@8743
   157
nipkow@8743
   158
Terms may also contain
nipkow@8743
   159
\isasymlambda-abstractions\indexbold{$Isalam@\isasymlambda}. For example,
nipkow@8771
   160
\isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and
nipkow@8771
   161
returns \isa{x+1}. Instead of
nipkow@8771
   162
\isa{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.~$t$} we can write
nipkow@8771
   163
\isa{\isasymlambda{}x~y~z.~$t$}.
nipkow@8743
   164
nipkow@8771
   165
\textbf{Formulae}\indexbold{formula} are terms of type \isaindexbold{bool}.
nipkow@8771
   166
There are the basic constants \isaindexbold{True} and \isaindexbold{False} and
nipkow@8771
   167
the usual logical connectives (in decreasing order of priority):
nipkow@8771
   168
\indexboldpos{\isasymnot}{$HOL0not}, \indexboldpos{\isasymand}{$HOL0and},
nipkow@8771
   169
\indexboldpos{\isasymor}{$HOL0or}, and \indexboldpos{\isasymimp}{$HOL0imp},
nipkow@8743
   170
all of which (except the unary \isasymnot) associate to the right. In
nipkow@8771
   171
particular \isa{A \isasymimp~B \isasymimp~C} means \isa{A \isasymimp~(B
nipkow@8771
   172
  \isasymimp~C)} and is thus logically equivalent to \isa{A \isasymand~B
nipkow@8771
   173
  \isasymimp~C} (which is \isa{(A \isasymand~B) \isasymimp~C}).
nipkow@8743
   174
nipkow@8743
   175
Equality is available in the form of the infix function
nipkow@8771
   176
\isa{=}\indexbold{$HOL0eq@\texttt{=}} of type \isa{'a \isasymFun~'a
nipkow@8771
   177
  \isasymFun~bool}. Thus \isa{$t@1$ = $t@2$} is a formula provided $t@1$
nipkow@8743
   178
and $t@2$ are terms of the same type. In case $t@1$ and $t@2$ are of type
nipkow@8771
   179
\isa{bool}, \isa{=} acts as if-and-only-if. The formula
nipkow@8771
   180
\isa{$t@1$~\isasymnoteq~$t@2$} is merely an abbreviation for
nipkow@8771
   181
\isa{\isasymnot($t@1$ = $t@2$)}.
nipkow@8743
   182
paulson@10795
   183
Quantifiers are written as
nipkow@8771
   184
\isa{\isasymforall{}x.~$P$}\indexbold{$HOL0All@\isasymforall} and
nipkow@8771
   185
\isa{\isasymexists{}x.~$P$}\indexbold{$HOL0Ex@\isasymexists}.  There is
nipkow@8771
   186
even \isa{\isasymuniqex{}x.~$P$}\index{$HOL0ExU@\isasymuniqex|bold}, which
nipkow@8771
   187
means that there exists exactly one \isa{x} that satisfies \isa{$P$}.  Nested
nipkow@8771
   188
quantifications can be abbreviated: \isa{\isasymforall{}x~y~z.~$P$} means
nipkow@8771
   189
\isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}.
nipkow@8743
   190
nipkow@8743
   191
Despite type inference, it is sometimes necessary to attach explicit
nipkow@8771
   192
\textbf{type constraints}\indexbold{type constraint} to a term.  The syntax is
nipkow@8771
   193
\isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that
nipkow@10538
   194
\ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed
nipkow@8771
   195
in parentheses: \isa{x < y::nat} is ill-typed because it is interpreted as
paulson@10795
   196
\isa{(x < y)::nat}. The main reason for type constraints is overloading of
nipkow@10538
   197
functions like \isa{+}, \isa{*} and \isa{<}. See {\S}\ref{sec:overloading} for
nipkow@10695
   198
a full discussion of overloading and Table~\ref{tab:overloading} for the most
nipkow@10695
   199
important overloaded function symbols.
nipkow@8743
   200
nipkow@8743
   201
\begin{warn}
nipkow@8743
   202
In general, HOL's concrete syntax tries to follow the conventions of
nipkow@8743
   203
functional programming and mathematics. Below we list the main rules that you
nipkow@8743
   204
should be familiar with to avoid certain syntactic traps. A particular
nipkow@8743
   205
problem for novices can be the priority of operators. If you are unsure, use
paulson@10795
   206
additional parentheses. In those cases where Isabelle echoes your
nipkow@10971
   207
input, you can see which parentheses are dropped --- they were superfluous. If
nipkow@8743
   208
you are unsure how to interpret Isabelle's output because you don't know
paulson@10795
   209
where the (dropped) parentheses go, set the \rmindex{flag}
nipkow@9792
   210
\isaindexbold{show_brackets}:
nipkow@8743
   211
\begin{ttbox}
nipkow@8743
   212
ML "set show_brackets"; \(\dots\); ML "reset show_brackets";
nipkow@8743
   213
\end{ttbox}
nipkow@8743
   214
\end{warn}
nipkow@8743
   215
nipkow@8743
   216
\begin{itemize}
nipkow@8743
   217
\item
nipkow@8771
   218
Remember that \isa{f t u} means \isa{(f t) u} and not \isa{f(t u)}!
nipkow@8743
   219
\item
nipkow@8771
   220
Isabelle allows infix functions like \isa{+}. The prefix form of function
nipkow@8771
   221
application binds more strongly than anything else and hence \isa{f~x + y}
nipkow@8771
   222
means \isa{(f~x)~+~y} and not \isa{f(x+y)}.
nipkow@8743
   223
\item Remember that in HOL if-and-only-if is expressed using equality.  But
nipkow@8743
   224
  equality has a high priority, as befitting a relation, while if-and-only-if
nipkow@8771
   225
  typically has the lowest priority.  Thus, \isa{\isasymnot~\isasymnot~P =
nipkow@8771
   226
    P} means \isa{\isasymnot\isasymnot(P = P)} and not
nipkow@8771
   227
  \isa{(\isasymnot\isasymnot P) = P}. When using \isa{=} to mean
nipkow@8771
   228
  logical equivalence, enclose both operands in parentheses, as in \isa{(A
nipkow@8743
   229
    \isasymand~B) = (B \isasymand~A)}.
nipkow@8743
   230
\item
nipkow@8743
   231
Constructs with an opening but without a closing delimiter bind very weakly
nipkow@8743
   232
and should therefore be enclosed in parentheses if they appear in subterms, as
nipkow@10971
   233
in \isa{(\isasymlambda{}x.~x) = f}. This includes \isaindex{if},
nipkow@8771
   234
\isaindex{let}, \isaindex{case}, \isa{\isasymlambda}, and quantifiers.
nipkow@8743
   235
\item
nipkow@8771
   236
Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}
nipkow@8771
   237
because \isa{x.x} is always read as a single qualified identifier that
nipkow@8771
   238
refers to an item \isa{x} in theory \isa{x}. Write
nipkow@8771
   239
\isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead.
nipkow@8771
   240
\item Identifiers\indexbold{identifier} may contain \isa{_} and \isa{'}.
nipkow@8743
   241
\end{itemize}
nipkow@8743
   242
nipkow@8771
   243
For the sake of readability the usual mathematical symbols are used throughout
nipkow@10983
   244
the tutorial. Their \textsc{ascii}-equivalents are shown in table~\ref{tab:ascii} in
nipkow@8771
   245
the appendix.
nipkow@8771
   246
nipkow@8743
   247
nipkow@8743
   248
\section{Variables}
nipkow@8743
   249
\label{sec:variables}
nipkow@8743
   250
\indexbold{variable}
nipkow@8743
   251
nipkow@8743
   252
Isabelle distinguishes free and bound variables just as is customary. Bound
nipkow@8743
   253
variables are automatically renamed to avoid clashes with free variables. In
nipkow@8743
   254
addition, Isabelle has a third kind of variable, called a \bfindex{schematic
nipkow@8743
   255
  variable}\indexbold{variable!schematic} or \bfindex{unknown}, which starts
nipkow@8771
   256
with a \isa{?}.  Logically, an unknown is a free variable. But it may be
nipkow@8743
   257
instantiated by another term during the proof process. For example, the
nipkow@8771
   258
mathematical theorem $x = x$ is represented in Isabelle as \isa{?x = ?x},
nipkow@8743
   259
which means that Isabelle can instantiate it arbitrarily. This is in contrast
nipkow@8743
   260
to ordinary variables, which remain fixed. The programming language Prolog
nipkow@8743
   261
calls unknowns {\em logical\/} variables.
nipkow@8743
   262
nipkow@8743
   263
Most of the time you can and should ignore unknowns and work with ordinary
nipkow@8743
   264
variables. Just don't be surprised that after you have finished the proof of
nipkow@8743
   265
a theorem, Isabelle will turn your free variables into unknowns: it merely
nipkow@8743
   266
indicates that Isabelle will automatically instantiate those unknowns
nipkow@8743
   267
suitably when the theorem is used in some other proof.
nipkow@9689
   268
Note that for readability we often drop the \isa{?}s when displaying a theorem.
nipkow@8743
   269
\begin{warn}
nipkow@8771
   270
  If you use \isa{?}\index{$HOL0Ex@\texttt{?}} as an existential
nipkow@8771
   271
  quantifier, it needs to be followed by a space. Otherwise \isa{?x} is
nipkow@8743
   272
  interpreted as a schematic variable.
nipkow@8743
   273
\end{warn}
nipkow@8743
   274
paulson@10885
   275
\section{Interaction and Interfaces}
nipkow@8771
   276
nipkow@8771
   277
Interaction with Isabelle can either occur at the shell level or through more
nipkow@8771
   278
advanced interfaces. To keep the tutorial independent of the interface we
nipkow@8771
   279
have phrased the description of the intraction in a neutral language. For
nipkow@8771
   280
example, the phrase ``to abandon a proof'' means to type \isacommand{oops} at the
nipkow@8771
   281
shell level, which is explained the first time the phrase is used. Other
nipkow@8771
   282
interfaces perform the same act by cursor movements and/or mouse clicks.
nipkow@8771
   283
Although shell-based interaction is quite feasible for the kind of proof
nipkow@8771
   284
scripts currently presented in this tutorial, the recommended interface for
nipkow@8771
   285
Isabelle/Isar is the Emacs-based \bfindex{Proof
nipkow@8771
   286
  General}~\cite{Aspinall:TACAS:2000,proofgeneral}.
nipkow@8771
   287
nipkow@8771
   288
Some interfaces (including the shell level) offer special fonts with
nipkow@10983
   289
mathematical symbols. For those that do not, remember that \textsc{ascii}-equivalents
nipkow@10978
   290
are shown in table~\ref{tab:ascii} in the appendix.
nipkow@8771
   291
nipkow@9541
   292
Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} 
nipkow@9541
   293
Commands may but need not be terminated by semicolons.
nipkow@9541
   294
At the shell level it is advisable to use semicolons to enforce that a command
nipkow@8771
   295
is executed immediately; otherwise Isabelle may wait for the next keyword
nipkow@9541
   296
before it knows that the command is complete.
nipkow@8771
   297
nipkow@8771
   298
paulson@10885
   299
\section{Getting Started}
nipkow@8743
   300
nipkow@8743
   301
Assuming you have installed Isabelle, you start it by typing \texttt{isabelle
nipkow@8743
   302
  -I HOL} in a shell window.\footnote{Simply executing \texttt{isabelle -I}
nipkow@8743
   303
  starts the default logic, which usually is already \texttt{HOL}.  This is
nipkow@8743
   304
  controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle
nipkow@8743
   305
    System Manual} for more details.} This presents you with Isabelle's most
nipkow@10983
   306
basic \textsc{ascii} interface.  In addition you need to open an editor window to
nipkow@8743
   307
create theory files.  While you are developing a theory, we recommend to
nipkow@8743
   308
type each command into the file first and then enter it into Isabelle by
nipkow@8743
   309
copy-and-paste, thus ensuring that you have a complete record of your theory.
nipkow@8771
   310
As mentioned above, Proof General offers a much superior interface.
paulson@10795
   311
If you have installed Proof General, you can start it by typing \texttt{Isabelle}.