From 6141b20b97247820a388d2b8680f24711b404576 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 29 May 2001 17:52:51 +0000
Subject: Fix layout and typo.

---
 html/features.html | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

(limited to 'html/features.html')

diff --git a/html/features.html b/html/features.html
index cd8a999c..cc38adde 100644
--- a/html/features.html
+++ b/html/features.html
@@ -29,9 +29,10 @@ you'd like an interface with the following features...
   <p>
   Take a look at these
   <a href="screenshot.html">screenshots</a>
-  of Proof General to see script managament in action.
+  of Proof General to see script management in action.
   </p>
   </dd>
+</dl><dl>
   <?php dt("Simplified interaction","simple") ?>
   <dd>
   Proof General is designed for proof assistants which have a
@@ -50,7 +51,8 @@ you'd like an interface with the following features...
   commandeer the proof assistant shell: the user still has complete
   access to it if necessary.
   </p>
-</dd>
+  </dd>
+</dl><dl>
   <?php dt("Multiple files","multiple") ?>
   <dd>
   Script management in Proof General can work across many script
@@ -65,6 +67,7 @@ you'd like an interface with the following features...
   Proof General (based on the order in which files were processed).
   </p>
   </dd>
+</dl><dl>
   <?php dt("Proof by Pointing","pbp") ?>
   <dd>
   <em>Proof by pointing</em> allows you to click on a subterm of
@@ -79,6 +82,7 @@ you'd like an interface with the following features...
   <?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.  Please canvas the implementor of your favourite 
 proof assistant to add PBP support.")  ?>
   </dd>
+</dl><dl>
   <?php dt("Toolbar and menus","toolbar") ?>
   <dd>
   Proof General has a toolbar with buttons for examining
@@ -95,6 +99,7 @@ proof assistant to add PBP support.")  ?>
   </p>
   <?php footnote("Toolbar is available in XEmacs only") ?>
   </dd>
+</dl><dl>
   <?php dt("Syntax highlighting","fontlock") ?>
   <dd>
   Syntax highlighting is an editing feature which decorates a file
@@ -106,6 +111,7 @@ proof assistant to add PBP support.")  ?>
   assumptions, for example.
   </p>
   </dd>
+</dl><dl>
   <?php dt("Real symbols","xsymbol") ?>
   <dd>
   Proof General has a close integration with the
@@ -123,6 +129,7 @@ proof assistant to add PBP support.")  ?>
   <p>
   <?php footnote("X-Symbol currently works in XEmacs only") ?>
   </dd>
+</dl><dl>
   <?php dt("Functions Menu","funcmenu") ?>
   <dd>
   A pull-down menu gives easy
@@ -132,6 +139,7 @@ proof assistant to add PBP support.")  ?>
 <!--   <?php footnote("Definitions menu is available in XEmacs only") ?> -->
   <p>
   </dd>
+</dl><dl>
   <?php dt("Remote proof assistant.") ?>
   <dd>
   Sometimes you may want to run a proof assistant on a powerful remote
@@ -139,6 +147,7 @@ proof assistant to add PBP support.")  ?>
   remotely, while your files and editor reside on your local machine.
   <p></p>
   </dd>
+</dl><dl>
   <?php dt("Tags","tags") ?>
   <dd>
   Tags are an editing feature which allow you to quickly locate the
@@ -150,6 +159,7 @@ proof assistant to add PBP support.")  ?>
 <!--   <?php footnote("Tags programs are provided for LEGO and Coq") ?> -->
   <p></p>
   </dd>
+</dl><dl>
   <?php dt("Adaptability","generic") ?>
   <dd>
   Proof General is designed to be adaptable.  Many aspects
-- 
cgit v1.2.3