Next: HOL Light Proof General, Previous: Coq Proof General, 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.
Isabelle provides its own way to invoke Proof General via the
isabelle
command. Running isabelle emacs
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. Proof General provides reliable control over incremental execution of the text.
When you load an Isabelle theory file into Proof General, you may be
prompted for the path to the program isabelle
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 isabelle findlogics
.
(Similarly, the documentation menu is partly generated from
isabelle 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 isabelle
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 does not work for you, perhaps because isabelle is not on your path, or you are running it remotely.
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:
(* -*- isabelle-chosen-logic
: "ZF" -*- *)
The default value is nil
.
Adjust isabelle-prog-name and proof-prog-name
for running logic.
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 Tokens package will provide immediate visual feedback.
Inserts "\<^bold>" (bold character)
Inserts "\<^loc>" (“local” control)
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.
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.
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.
Previous: Isabelle settings, Up: Isabelle Proof General [Contents][Index]