[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Isabelle Proof General supports major generic features of Proof General, including integration with Isabelle's theory loader for proper automatic multiple file handling. Support for tags and proof-by-pointing is missing.
In this version, support for the old-style “classic” Isabelle theory files has been removed; in Isabelle2007 only Isar style theory files are supported.
Isabelle provides its own way to invoke Proof General via the
Isabelle
script. Running Isabelle
starts an Emacs session
with Isabelle Proof General. The defaults may be changed by editing the
Isabelle settings, see the Isabelle documentation for details.
Proof General for Isabelle manages Isar ‘.thy’ files. The syntax of Isabelle input is technically simple, enabling Proof General to provide reliable control over incremental execution of the text. Thus it is very hard to let Proof General lose synchronization with the Isabelle process.
10.1 Choosing logic and starting isabelle | ||
10.2 Isabelle commands | ||
10.3 Isabelle settings | ||
10.4 Isabelle customizations |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
When you load an Isabelle theory file into Proof General, you may be
prompted for the path to the program isatool
if it is not on the
system PATH
already. This is used to generate further
information for invoking Isabelle, in particular, the list of available
logics.
The Isabelle menu offers an easy way to select the invoked object logic. If you look at the menu:
Isabelle -> Logics -> |
you should see the list of logics available to Isabelle. This menu is
generated from the output of the command isatool findlogics
.
(Similarly, the documentation menu is partly generated from
isatool doc
). Instead of the menu, you can use the
keyboard command isabelle-chose-logic
to choose from the list.
The logics list is refreshed dynamically so you can select any newly built heap images in the same Emacs session. However, notice that the choices are greyed out while Isabelle is actually runnning — you can only switch to a new logic if you first exit Isabelle (similarly to Proof General, Isabelle operates with only one logic at a time).
Another way to set the logic before Isabelle is launched is using an
Emacs local variable setting inside a comment at the top of the file,
see the documentation of isabelle-chosen-logic
below.
In case you do not have the isatool
program available or want to
override its behaviour, you may set the variable
isabelle-program-name-override
to define the name of the
executable used to start Isabelle. The standard options are and
logic name are still appended.
Name of executable program to run Isabelle.
You can set customize this in case the automatic settings mechanism (based on isatool) does not work for you. One reason to do this is if you are running Isabelle remotely, or using windows and avoiding isatool.
A possible value when running under Windows looks like this:
C:\sml\bin\.run\run.x86-win32.exe @SMLload=C:\Isabelle\ |
This expects SML/NJ in C:\sml and Isabelle images in C:Isabelle. The logic image name is tagged onto the end.
The default value is nil
.
Choice of logic to use with Isabelle.
If non-nil, added onto the Isabelle command line for invoking Isabelle.
You can set this as a file local variable, using a special comment at the top of your theory file, like this:
(* -*- |
The default value is nil
.
Adjust isabelle-prog-name
and proof-prog-name
for running logic.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The Isabelle instance of Proof General supplies several specific help key bindings; these functions are offered within the prover help menu as well.
Invokes Isar command refute
on the current subgoal. Only available in HOL
and derived logics.
Invokes Isar command quickcheck
on the current subgoal.
Displays a draft document of the current theory.
Prints a draft document of the current theory.
Shows available antiquotation commands and options.
Shows the current Classical Reasoner context.
Shows the current set of induct/cases rules.
Shows the current Simplifier context.
Shows the current set of transitivity rules (for calculational reasoning).
Shows attributes available in current theory context.
Shows all local term bindings.
Shows all named local contexts (cases).
Shows all local facts.
Shows inner syntax of the current theory context (for types and terms).
Shows proof methods available in current theory context.
Shows all available commands of Isabelle's outer syntax.
Shows theorems stored in the current theory node.
Invoke sledgehammer on first subgoal.
Find theorems containing given arguments (prompt in minibuffer).
Invokes the thms_containing
command. Arguments are
separated by white space as usual in Isar.
Find theorems containing (argument in form)
Find theorems: either of the above.
The following shortcuts insert control sequences into the text, modifying the appearance of individual symbols (single letters, mathematical entities etc.); the X-Symbol package will provide immediate visual feedback.
Inserts "\<^bold>"
Inserts "\<^loc>"
Inserts "\<^sup>" (superscript character)
Inserts "\<^sub>" (subscript character)
Inserts "\<^bsup> \<^esup>" (superscript string)
Inserts "\<^bsub> \<^esub>" (subscript string)
Inserts "\<^isub>" (identifier subscript letter)
Inserts "\<^raw:>" (raw LaTeX text)
Inserts "@{text ""}" (anti-quotation).
Inserts "ML {* *}" (inline ML code).
Command termination via `;
' is an optional feature of Isar
syntax. Neither Isabelle nor Proof General require semicolons to
do their job. The following command allows to get rid of command
terminators in existing texts.
Remove explicit Isabelle/Isar command terminators ‘;’ from the buffer.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The Isabelle menu also contains a Settings
submenu, which
allows you to configure things such as the behaviour of Isabelle's term
pretty printer (display of types, sorts, etc). Note that you won't
see this sub-menu until Isabelle has been started, because it is
generated by Isabelle itself. Proof General, on the other hand, is
responsible for recording any settings that are configured when you
select Isabelle -> Settings -> Save Settings
. They are stored
along with the other Emacs customization settings.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Here are some of the other user options specific to Isabelle. You can set these as usual with the customization mechanism.
URL of web page for Isabelle.
[ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This document was generated by David Aspinall on July, 24 2008 using texi2html 1.78.