Deleted file

1 files changed, 0 insertions, 52 deletions

diff --git a/README.exper b/README.exper
deleted file mode 100644
index f571a701..00000000
--- a/README.exper
+++ /dev/null
@@ -1,52 +0,0 @@
-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 `nil', and restart
-Proof General, then the features mentioned below will be disabled.
-
-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
-===============================
-
-** "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.
-
-   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
-   some information.  The information in Isabelle/Isar is the type of
-   the variable, often, but it depends on the context and may be
-   wrong.  In Isabelle/classic the type information is useless.
-   This feature is a vague hint of what could be done with proper subterm
-   markup from the Isabelle engine.  Without this, it cannot work
-   well, because no context is available for Proof General to send
-   back to the prover, so only variables bound at the outer level can 
-   have sensible information displayed, via the "term" command.
-
-
-Known problems with experimental features
-=========================================
-
-** Move up/down functions may spoil visibility behaviour.
-   
\ No newline at end of file