From 355c89f4ad30f7783c9beadf1d105e8dc6f2a127 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 1 Dec 1999 19:14:33 +0000
Subject: Fix HTML errors.

---
 html/features.phtml | 27 ++++++++++++++-------------
 1 file changed, 14 insertions(+), 13 deletions(-)

(limited to 'html/features.phtml')

diff --git a/html/features.phtml b/html/features.phtml
index c647d9ac..63426bf6 100644
--- a/html/features.phtml
+++ b/html/features.phtml
@@ -24,9 +24,8 @@ and finally,
 Are you convinced yet?
 If not, read on…
 </p>
-</hrule>
 <dl>
-  <a name="simple"><?php dt("Simplfied interaction.") ?></a> 
+  <?php dt("Simplified interaction.","simple") ?>
   <dd>
   Proof General is designed for proof assistants which have a
   command-line shell interpreter.  When using Proof General, the proof
@@ -45,7 +44,7 @@ If not, read on&#8230;
   access to it if necessary.
   </p>
 </dd>
-  <a name="script"><?php dt("Script management.") ?></a>
+  <?php dt("Script management.","script") ?>
   <dd>
   A <em>proof script</em> is a sequence of commands sent to
   a proof assistant to construct a proof, usually stored in
@@ -67,7 +66,7 @@ If not, read on&#8230;
   of Proof General to see script managament in action.
   </p>
   </dd>
-  <a name="multiple"><?php dt("Multiple files.") ?></a>
+  <?php dt("Multiple files.","multiple") ?>
   <dd>
   Script management in Proof General can work across many script
   files.  When a script is visited in the editor, it is locked
@@ -80,7 +79,7 @@ If not, read on&#8230;
   Proof General (based on the order in which files were processed).
   </p>
   </dd>
-  <a name="pbp"><?php dt("Proof by Pointing.") ?></a>
+  <?php dt("Proof by Pointing.","pbp") ?>
   <dd>
   <em>Proof by pointing</em> allows you to click on a subterm of
   a goal to be proved, and apply an appropriate rule or 
@@ -93,7 +92,7 @@ If not, read on&#8230;
   </p>
   <?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>
+  <?php dt("Toolbar and menus.","toolbar") ?>
   <dd>
   Proof General has a toolbar with buttons for examining
   the proof state, starting a proof, manoeuvring in the proof script, 
@@ -109,7 +108,7 @@ If not, read on&#8230;
   </p>
   <?php footnote("Toolbar is available in XEmacs only") ?>
   </dd>
-  <a name="fontlock"><?php dt("Syntax highlighting.") ?></a>
+  <?php dt("Syntax highlighting.","fontlock") ?>
   <dd>
   Syntax highlighting is an editing feature which decorates a file
   with different colours or fonts according to the syntax of some
@@ -120,21 +119,23 @@ If not, read on&#8230;
   assumptions, for example.
   </p>
   </dd>
-  <a name="xsymbol"><?php dt("Real symbols.") ?></a>
+  <?php dt("Real symbols.","xsymbol") ?>
   <dd>
   Proof General has a close integration with the
   powerful 
   <a href="http://www.fmi.uni-passau.de/~wedler/x-symbol">X-Symbol</a>
   package, which makes it easy to transparently use real symbols and
   Greek letters in your proofs.  
-  <br> Instead of seeing "not P", you see "&not; </dd>P", instead
-    of "a * b", you see "a &times; b", etc. <br>
+  <br> 
+  Instead of seeing "not P", you see "&not; P", instead
+   of "a * b", you see "a &times; b", etc. 
+  <br>
    [the examples above are simple so they will work on most browsers 
     without needing images]
   <p>
   <?php footnote("X-Symbol currently works in XEmacs only") ?>
   </dd>
-  <a name="funcmenu"><?php dt("Functions Menu.") ?></a>
+  <?php dt("Functions Menu.","funcmenu") ?>
   <dd>
   A pull-down menu gives easy
   navigations to theorems, definitions, and declarations
@@ -150,7 +151,7 @@ If not, read on&#8230;
   remotely, while your files and editor reside on your local machine.
   <p></p>
   </dd>
-  <a name="tags"><?php dt("Tags.") ?></a>
+  <?php dt("Tags.","tags") ?>
   <dd>
   Tags are an editing feature which allow you to quickly locate the
   definition or declaration of a particular identifier.  Proof General
@@ -161,7 +162,7 @@ If not, read on&#8230;
 <!--   <?php footnote("Tags programs are provided for LEGO and Coq") ?> -->
   <p></p>
   </dd>
-  <a name="generic"><?php dt("Adaptability.") ?></a>
+  <?php dt("Adaptability.","generic") ?>
   <dd>
   Proof General is designed to be adaptable.  Many aspects
   of its behaviour can be easily customized (using dialogue boxes and
-- 
cgit v1.2.3