aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Aspinall2000-03-14 10:55:35 +0000
committerDavid Aspinall2000-03-14 10:55:35 +0000
commit0ed3156faa289a4fa04af018515a07e8904fff1f (patch)
tree336cd47444ab502db4e9ef6538b6b777effc0ec9
parent637359b517d597be8fb0ef80afd6ce64e17c0c1c (diff)
Updated
-rw-r--r--TODO3
-rw-r--r--html/mission.phtml4
2 files changed, 4 insertions, 3 deletions
diff --git a/TODO b/TODO
index 3d97dd78..3d61aad0 100644
--- a/TODO
+++ b/TODO
@@ -15,6 +15,9 @@ proofgen@dcs.ed.ac.uk. Thanks!
Plans for upcoming 3.x versions
-------------------------------
+* Support turning on/off prover output automatically, e.g.
+ Coq's "Begin Silent" and "End Silent" commands.
+
* Make an XEmacs package
* Support more proof assistants
diff --git a/html/mission.phtml b/html/mission.phtml
index 00f7b60f..deec79dc 100644
--- a/html/mission.phtml
+++ b/html/mission.phtml
@@ -40,9 +40,7 @@ Be a <a href="#quality"><i>high-quality</i></a> research prototype.
<p>
Above all, we take a <i>pragmatic</i> approach to constructing
interfaces. Our primary aim is to provide a tool which is
-immediately useful for proof engineering, rather than
-to provide publications by conducting research in
-human-computer interaction.
+immediately useful for proof engineering.
</p>
<p>
This aim means that we harness a range of