diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2004-04-02 16:58:54 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2004-04-02 16:58:54 +0000 |
commit | 2a5709c354e09b06556f3f1e19bf2d9a5ad91564 (patch) | |
tree | 7c401cc749ec9a5a7ab2fcf127a04eb0ac298b67 /README.exper | |
parent | b33e3f1c7f799aa3e0f3c70e023fa6a50cb308ad (diff) |
Updated.
Diffstat (limited to 'README.exper')
-rw-r--r-- | README.exper | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/README.exper b/README.exper index 2b6c718c..f571a701 100644 --- a/README.exper +++ b/README.exper @@ -7,12 +7,12 @@ 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. +`proof-experimental-features'. If you set this to `nil', and restart +Proof General, then the features mentioned below will be disabled. -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). +We encourage users to work with this flag set 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 @@ -28,10 +28,10 @@ Current "experimental" features in orange. This allows easy editing of theories to remove dead lemmas, re-order proofs, etc. - This only works for a pre-release version of Isabelle at the moment. - (Support is required from other proof assistant authors: please - mention to them). You must select the Isabelle setting - "Theorem Dependencies". + This only works in Isabelle at the moment. (Support is required + from other proof assistant authors: please suggest to them!). You + must select the Isabelle setting "Theorem Dependencies" before + starting Isabelle, to enable gathering of data. ** Active highlighting for variables in Isabelle. Moving the mouse over variables in the goal display will display |