aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Aspinall1999-11-17 17:33:06 +0000
committerDavid Aspinall1999-11-17 17:33:06 +0000
commit106599933a20433fa8adc213e0b05c4179fccd5f (patch)
treef6bd59b9c6609334f15b5f9753229605534fc544
parent6cbd3fcffef57123dfe37c87e05f43996a2eda1c (diff)
Link to demoisa-easy.el
-rw-r--r--html/features.phtml9
1 files changed, 8 insertions, 1 deletions
diff --git a/html/features.phtml b/html/features.phtml
index 0b3fee7d..f4fca86e 100644
--- a/html/features.phtml
+++ b/html/features.phtml
@@ -153,7 +153,14 @@ If not, read on…
the prover, and setting other variables with commands to send to the
prover. To get the most from Proof General (proof by pointing, for
example), it may be necessary to augment the output routines of the
- proof assistant.
+ proof assistant.
+ </p>
+ <p>
+ New! With Proof General 3.0, adapting to a new prover is easier
+ than ever before!
+ <a href="ProofGeneral/demoisa/demoisa-easy.el">Here</a>
+ is an example instance of Proof General for Isabelle, which
+ configures the main core of the interface.
</p>
Please feel free to download Proof General to customize it for a new
system, and