From 610822c84da30599179500c596109c31c9b4d7da Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 17 Nov 1999 19:52:56 +0000
Subject: Link to demoisa-easy.el

---
 html/features.phtml | 23 ++++++++++-------------
 html/news.phtml     | 10 ++++++++++
 2 files changed, 20 insertions(+), 13 deletions(-)

(limited to 'html')

diff --git a/html/features.phtml b/html/features.phtml
index f4fca86e..a8631cbc 100644
--- a/html/features.phtml
+++ b/html/features.phtml
@@ -71,7 +71,7 @@ If not, read on…
   Proof General also uses the subterm structure to make it easy to cut
   and paste from complicated terms.
   </p>
-  <?php footnote("Proof by pointing for Proof General is only supported by LEGO (experimentally) at the moment.  We need help from each proof assistant implementors to add it elsewhere.")  ?>
+  <?php footnote("Proof by pointing for Proof General is only supported by LEGO (experimentally) at the moment.  For others, we need help from each proof assistant implementor to add support for their system.")  ?>
   </dd>
   <a name="toolbar"><?php dt("Toolbar and menus") ?></a>
   <dd>
@@ -119,7 +119,8 @@ If not, read on&#8230;
   A pull-down menu gives easy
   access to definitions, declarations and proofs in the current
   buffer.  
-  <?php footnote("Definitions menu is available in XEmacs only") ?>
+<!-- it is in FSF Emacs if you download func-menu.el from somewhere -->
+<!--   <?php footnote("Definitions menu is available in XEmacs only") ?> -->
   </dd>
   <?php dt("Remote proof assistant.") ?>
   <dd>
@@ -146,21 +147,17 @@ If not, read on&#8230;
   buttons, no text file editing!).   
   <p>
   Most importantly, Proof General is generic, so you can adapt it to 
-  a new proof assistant with surprisingly little effort.
+  a new proof assistant with surprisingly little effort
   <p>
   Adapting for a new proof assistant is mainly a matter of setting
   some variables with regular expressions to help parse output from
   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.  
-  </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.
+  prover.  See this basic
+ <?php fileshow("ProofGeneral/demoisa/demoisa-easy.el", 
+	  "example instance"); ?>.
+  To get the most from Proof General (proof by pointing, for
+  example), it may be necessary to put some hooks in
+  the output routines of the proof assistant.  
   </p>
   Please feel free to download Proof General to customize it for a new
   system, and 
diff --git a/html/news.phtml b/html/news.phtml
index 223235fe..774da996 100644
--- a/html/news.phtml
+++ b/html/news.phtml
@@ -6,6 +6,16 @@
 </p>
 
 <ul>
+<li><b>17th November 1999</b><br>
+<p>
+  New!  With Proof General 3.0, adapting to a new prover is easier
+  than ever before!
+  It includes an 
+ <?php fileshow("ProofGeneral/demoisa/demoisa-easy.el", "example instance"); ?>
+  of Proof General for Isabelle, which 
+  configures the main core of the interface with less than 30 lines of
+  code.  Not bad for getting about 4000 lines worth of code from it!
+</p>
 <li><b>15th November 1999</b><br>
 <p>
 Proof General 3.0 is currently in testing, and will be released later
-- 
cgit v1.2.3