aboutsummaryrefslogtreecommitdiffhomepage
path: root/hol98
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2007-12-13 12:58:11 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2007-12-13 12:58:11 +0000
commitd64389d34f3494b97c67b7a6094123f1a699040c (patch)
tree67c8fd95283d89a960240200970a9a2b134cb67b /hol98
parent44d5bf78ff00eb2d48f111d8d8718aa3b8ad010c (diff)
Deleted file
Diffstat (limited to 'hol98')
-rw-r--r--hol98/todo25
1 files changed, 0 insertions, 25 deletions
diff --git a/hol98/todo b/hol98/todo
deleted file mode 100644
index d65df204..00000000
--- a/hol98/todo
+++ /dev/null
@@ -1,25 +0,0 @@
--*- mode:outline -*-
-
-* Things to do for HOL
-
-See also ../todo for generic things to do, priority codes.
-
-** A Problem with process filtering.
-
- Process (sometimes?) doesn't recover after interrupt, and no output
- is seen. Why?
-
- Also problem with some input texts: try interactive version of
- clScript.sml, inductive defn of CL terms breaks things.
-
-** B Improve display to strip ugly val it and spurious >'s.
-
-** B Add special markup to improve robustness
-
-** B Add support for multiple files
-
-** B Add support for proof by pointing.
-
-** B Output highlighting doesn't seem to work properly.
-
-