diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-08-12 08:33:46 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-08-12 08:33:46 +0000 |
| commit | d55abd121ba1a1c5ac49a52622d5e9cc526337aa (patch) | |
| tree | 6ed7c7383f928de3394966f90c8e42570b424ae3 /README.exper | |
| parent | 8c6b24410a2ef8d9767bfc1f4c12c0bfa6a0605c (diff) | |
Describe variable highlighting
Diffstat (limited to 'README.exper')
| -rw-r--r-- | README.exper | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/README.exper b/README.exper index 494ae0d8..79ef743d 100644 --- a/README.exper +++ b/README.exper @@ -33,6 +33,12 @@ Current "experimental" features You must select the Isabelle option "Theorem Dependencies", and then restart Isabelle. - - - +** Active highlighting for variables in Isabelle. + Moving the mouse over variables in the goal display will display + some information. The information in Isabelle/Isar is the type of + the variable, usually. In Isabelle it is useless. + This feature is a hint of what could be done with proper subterm + markup from the Isabelle engine. Without this, it cannot work + well, because no context is available to Proof General, so only + variables bound at the outer level can have meaningful information + displayed, via the "term" command. |