From 0ed3156faa289a4fa04af018515a07e8904fff1f Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 14 Mar 2000 10:55:35 +0000
Subject: Updated

---
 TODO               | 3 +++
 html/mission.phtml | 4 +---
 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 
-- 
cgit v1.2.3