diff options
Diffstat (limited to 'README.exper')
| -rw-r--r-- | README.exper | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/README.exper b/README.exper new file mode 100644 index 00000000..73b2e691 --- /dev/null +++ b/README.exper @@ -0,0 +1,30 @@ +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 + Only works for Isabelle/classic at the moment. You must also + select the Isabelle option "Theorem Dependencies". + + + |