From 573cc798a9feaa8371f145d8009f5726d10ee1ae Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 17 Jul 2002 12:27:10 +0000
Subject: Mention term highlighting

---
 CHANGES | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/CHANGES b/CHANGES
index 627d4bf3..124da18b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -45,13 +45,22 @@ For minor issues, see isa/BUGS.
 
 ** Isabelle Changes
 
-Isabelle/Isar syntax changes, other tweaks for Isabelle2002.
+*** Isabelle/Isar syntax changes, other tweaks for Isabelle2002.
+
 Switch to using Isabelle/Isar by default for .thy files.
 Support next error function.
 
 Isabelle classic mode: highlighting tweaks for ML code contributed by
 Lucas Dixon (lucasd@dai.ed.ac.uk)
 
+*** Active highlighting of variables
+
+Variables are made active in the goals buffer.  Hovering the mouse
+over an identifier shows its type.  [IN PROGRESS; faulty with X-Sym]
+
+This handy feature is a glimpse of what could be done with proper
+subterm markup, which needs support to be added in the Isabelle core.
+
 
 ** Coq Changes
 
-- 
cgit v1.2.3