diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1999-11-26 17:07:23 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1999-11-26 17:07:23 +0000 |
| commit | 138c69a571314874744376d5cdc723f52e885782 (patch) | |
| tree | bf20353f1bd4befbd125a69bbbe0f6878d15ca17 /html | |
| parent | 6f59d38e12b01e42d08a01fc35dce08d7c0abc62 (diff) | |
Fixup formatting
Diffstat (limited to 'html')
| -rw-r--r-- | html/features.phtml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/html/features.phtml b/html/features.phtml index e87d344d..bb6825ff 100644 --- a/html/features.phtml +++ b/html/features.phtml @@ -27,6 +27,7 @@ If not, read on… </hrule> <dl> <a name="simple"><?php dt("Simplfied interaction.") ?></a> + <dd> Proof General is designed for proof assistants which have a command-line shell interpreter. When using Proof General, the proof assistant's shell is hidden from the user. Communication takes @@ -38,7 +39,6 @@ If not, read on… displayed at once. This means that the user only sees the output from the most recent interaction, rather than a screen full of output from the proof assistant. - </p> <p> Despite more friendly communication model, Proof General does not commandeer the proof assistant shell: the user still has complete @@ -141,7 +141,7 @@ If not, read on… proved in the current buffer. <!-- it is in FSF Emacs if you download func-menu.el from somewhere --> <!-- <?php footnote("Definitions menu is available in XEmacs only") ?> --> - <p></p> + <p> </dd> <?php dt("Remote proof assistant.") ?> <dd> |