and is recommended browsing.

 and is recommended browsing. In subdirectory \texttt{Library} you find

 There is also a growing Library~\cite{HOL-Library}\index{Library}

 a growing library of useful theories that are not part of \isa{Main}

 of useful theories that are not part of \isa{Main} but can be included

 but can be included among the parents of a theory and will then be

 among the parents of a theory and will then be loaded automatically.

 loaded automatically.

   nonsense.  Isabelle insists that all terms and formulae must be well-typed

   nonsense.  Isabelle insists that all terms and formulae must be

   and will print an error message if a type mismatch is encountered. To

   well-typed and will print an error message if a type mismatch is

   reduce the amount of explicit type information that needs to be provided by

   encountered. To reduce the amount of explicit type information that

   the user, Isabelle infers the type of all variables automatically (this is

   needs to be provided by the user, Isabelle infers the type of all

   called \bfindex{type inference}) and keeps quiet about it. Occasionally

   variables automatically (this is called \bfindex{type inference})

   this may lead to misunderstandings between you and the system. If anything

   and keeps quiet about it. Occasionally this may lead to

   strange happens, we recommend that you ask Isabelle to display all type

   misunderstandings between you and the system. If anything strange

   information. This is best done through the Proof General interface; see

   happens, we recommend that you ask Isabelle to display all type

   \S\ref{sec:interface} for details.

   information via the Proof General menu item \textsf{Isabelle} $>$

   \textsf{Settings} $>$ \textsf{Show Types} (see \S\ref{sec:interface}

   for details).

 A particular

 A particular problem for novices can be the priority of operators. If

 problem for novices can be the priority of operators. If you are unsure, use

 you are unsure, use additional parentheses. In those cases where

 additional parentheses. In those cases where Isabelle echoes your

 Isabelle echoes your input, you can see which parentheses are dropped

 input, you can see which parentheses are dropped --- they were superfluous. If

 --- they were superfluous. If you are unsure how to interpret

 you are unsure how to interpret Isabelle's output because you don't know

 Isabelle's output because you don't know where the (dropped)

 where the (dropped) parentheses go, set the flag\index{flags}

 parentheses go, set the Proof General flag \textsf{Isabelle} $>$

 \isa{show_brackets}\index{*show_brackets (flag)}:

 \textsf{Settings} $>$ \textsf{Show Brackets} (see \S\ref{sec:interface}).

 \begin{ttbox}

 ML "set show_brackets"; \(\dots\); ML "reset show_brackets";

 \end{ttbox}

 Interaction with Isabelle can either occur at the shell level or through more

 The recommended interface for Isabelle/Isar is the (X)Emacs-based

 advanced interfaces. To keep the tutorial independent of the interface, we

 \bfindex{Proof General}~\cite{proofgeneral,Aspinall:TACAS:2000}.

 have phrased the description of the interaction in a neutral language. For

 Interaction with Isabelle at the shell level, although possible,

 example, the phrase ``to abandon a proof'' means to type \isacommand{oops} at the

 should be avoided. Most of the tutorial is independent of the

 shell level, which is explained the first time the phrase is used. Other

 interface and is phrased in a neutral language. For example, the

 interfaces perform the same act by cursor movements and/or mouse clicks.

 phrase ``to abandon a proof'' corresponds to the obvious

 Although shell-based interaction is quite feasible for the kind of proof

 action of clicking on the \textsf{Undo} symbol in Proof General.

 scripts currently presented in this tutorial, the recommended interface for

 Proof General specific information is often displayed in paragraphs

 Isabelle/Isar is the Emacs-based \bfindex{Proof

 identified by a miniature Proof General icon. Here are two examples:

   General}~\cite{proofgeneral,Aspinall:TACAS:2000}.

 Proof General specific information is always displayed in paragraphs

 Proof General supports a special font with mathematical symbols known

 identified by this miniature Proof General icon.

 as ``x-symbols''. All symbols have \textsc{ascii}-equivalents: for

 example, you can enter either \verb!&!  or \verb!\<and>! to obtain

 On particularly nice feature of Proof General is its support for a special

 $\land$. For a list of the most frequent symbols see table~\ref{tab:ascii}

 fonts with mathematical symbols. Most symbols have

 in the appendix.

 \textsc{ascii}-equivalents: for example, you can enter either \verb!&!

 or \verb!\<and>! to obtain $\land$. For a list of the most frequent symbols

 Note that by default x-symbols are not enabled. You have to switch

 see table~\ref{tab:ascii} in the appendix.

 them on via the menu item \textsf{Proof-General} $>$ \textsf{Options} $>$

 \textsf{X-Symbols} (and save the option via the top-level

 \textsf{Options} menu).

 Proof General offers an \texttt{Isabelle} menu for displaying information

 Proof General offers the \textsf{Isabelle} menu for displaying

 and setting flags. A particularly useful flag is \texttt{Show Types}

 information and setting flags. A particularly useful flag is

 which causes Isabelle to output the type information that is usually

 \textsf{Isabelle} $>$ \textsf{Settings} $>$ \textsf{Show Types} which

 causes Isabelle to output the type information that is usually

 because often the types reveal the source of the problem. Once you have

 because often the types reveal the source of the problem. Once you

 diagnosed the problem you may no longer want to see the types because they

 have diagnosed the problem you may no longer want to see the types

 clutter all output. Simply reset the flag.

 because they clutter all output. Simply reset the flag.

 Assuming you have installed Isabelle, you start it by typing \texttt{isabelle

 Assuming you have installed Isabelle and Proof General, you start it by typing

   -I HOL} in a shell window.\footnote{Simply executing \texttt{isabelle -I}

 \texttt{Isabelle} in a shell window. This launches a Proof General window.

   starts the default logic, which usually is already \texttt{HOL}.  This is

 By default, you are in HOL\footnote{This is controlled by the

   controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle

 \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle System Manual}

     System Manual} for more details.} This presents you with Isabelle's most

 for more details.}.

 basic \textsc{ascii} interface.  In addition you need to open an editor window to

 create theory files.  While you are developing a theory, we recommend that you

 \begin{pgnote}

 type each command into the file first and then enter it into Isabelle by

 You can choose a different logic via the \textsf{Isabelle} $>$

 copy-and-paste, thus ensuring that you have a complete record of your theory.

 \textsf{Logics} menu. For example, you may want to work in the real

 As mentioned above, Proof General offers a much superior interface.

 numbers, an extension of HOL (see \S\ref{sec:real}).

 If you have installed Proof General, you can start it by typing \texttt{Isabelle}.

 % This is just excess baggage:

 %(You have to restart Proof General if you only compile the new logic

 %after having launching Proof General already).

 \end{pgnote}