1 files changed, 52 insertions, 0 deletions
diff --git a/README.exper b/README.exper
new file mode 100644
index 00000000..2b6c718c
--- /dev/null
+++ b/README.exper
@@ -0,0 +1,52 @@
+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.
+
+   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".
+
+** 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