Improvements for type tokens, remove preceding colon

1 files changed, 6 insertions, 5 deletions

diff --git a/hol-light/README b/hol-light/README
index 59356fb7..238586c6 100644
--- a/hol-light/README
+++ b/hol-light/README
@@ -24,11 +24,12 @@ Notes:
 There are some problems at the moment.  HOL proof scripts often use
 batch-oriented single step tactic proofs, but Proof General does not
 offer an easy way to edit these kind of proofs.  The "Boomburg-HOL"
-Emacs interface by Koichi Takahashi and Masima Hagiya addressed this,
-and to some extent so perhaps does the Emacs interface supplied with
-HOL.  Perhaps one of these could be embedded/reimplemented inside
-Proof General.  Implemented in a generic way, managing batch vs
-interactive proofs might also be useful for other provers.
+Emacs interface by Koichi Takahashi and Masima Hagiya addressed this a
+long time ago, and to some extent so perhaps does the Emacs interface
+supplied with HOL.  Perhaps one of these could be
+embedded/reimplemented inside Proof General.  Implemented in a generic
+way, managing batch vs interactive proofs might also be useful for
+other provers.
 
 Another problem is that HOL scripts sometimes use OCaml modules, which
 will cause confusion because Proof General does not really parse OCaml,