Improvements for type tokens, remove preceding colon

3 files changed, 11 insertions, 10 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,
diff --git a/hol-light/hol-light-unicode-tokens.el b/hol-light/hol-light-unicode-tokens.el
index e6e3671d..df32e4bd 100644
--- a/hol-light/hol-light-unicode-tokens.el
+++ b/hol-light/hol-light-unicode-tokens.el
@@ -69,10 +69,10 @@
     ;; logic
     ("forall" "∀")
     ("exists" "∃")
-    (":num" ":ℕ" type) ;; ?
-    (":complex" ":ℂ" type)
-    (":real" ":ℝ" type)
-    (":int" ":ℤ" type)
+    ("num" "ℕ" type) ;; ?
+    ("complex" "ℂ" type)
+    ("real" "ℝ" type)
+    ("int" "ℤ" type)
     ("rat" "ℚ" type)
     ("bool" "B" underline type)
     ("false" "false" bold sans)
diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el
index 3201e2ff..85d10607 100644
--- a/hol-light/hol-light.el
+++ b/hol-light/hol-light.el
@@ -265,7 +265,7 @@ You need to restart Emacs if you change this setting."
    "CONJUNCT1" "CONJUNCT2" "CONJ_PAIR" "CONJUNCTS" "IMP_DEF" "MP"
    "DISCH" "DISCH_ALL" "UNDISCH" "UNDISCH_ALL" "IMP_ANTISYM_RULE" "ADD_ASSUM"
    "EQ_IMP_RULE" "IMP_TRANS" "FORALL_DEF" "SPEC" "SPECL" "SPEC_VAR"
-   "SPEC_ALL" "ISPEC" "ISPECL" "GEN" "GENL" "GEN_ALL th"
+   "SPEC_ALL" "ISPEC" "ISPECL" "GEN" "GENL" "GEN_ALL"
    "EXISTS_DEF" "EXISTS" "SIMPLE_EXISTS" "CHOOSE" "SIMPLE_CHOOSE" "OR_DEF"
    "DISJ1" "DISJ2" "DISJ_CASES" "SIMPLE_DISJ_CASES" "F_DEF" "NOT_DEF"
    "NOT_ELIM" "NOT_INTRO" "EQF_INTRO" "EQF_ELIM" "CONTR" "EXISTS_UNIQUE_DEF"