blob: 494ae0d8df7f5bbd4482da33e39fd80fad611d05 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
Experimental features in this release of Proof General.
======================================================
Proof General includes a few features designated as "experimental"
because they have not been fully tested or completed. Enabling these
will usually have no detrimental effects on using standard features of
PG, but the experimental features themselves may be less robust.
Experimental features can be enabled by customizing the variable
`proof-experimental-features'. If you set this to `t', and restart
Proof General, then the features mentioned below will be enabled.
We encourage users to set this flag and test the features, but being
aware that the features are regarded as incomplete (problem reports
and suggestions for improvements are welcomed).
Current "experimental" features
===============================
** "Move up" and "Move down" functions in context span menu
(use right-click on highlighted spans), also bound on
C-M-up/C-M-down.
** Theorem dependencies: displaying and highlighting dependencies.
Dependencies (e.g. lemmas) for a theorem are highlighted in
yellow, places where the theorem is used are highlighted
in orange. This allows easy editing of theories to remove
dead lemmas, re-order proofs, etc.
Only works for Isabelle/classic at the moment (support is
required from proof assistant authors: please mention to them).
You must select the Isabelle option "Theorem Dependencies",
and then restart Isabelle.
|
