diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-08-08 12:17:14 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-08-08 12:17:14 +0000 |
| commit | 60a84ffa180c02e7d78fadada20b58a238319bbf (patch) | |
| tree | c479bd45ecbb3dc2eaf246a4bd222ee8ba14deb7 /README.exper | |
| parent | aa6cc389e5620e38904014286d9e9b490ed48687 (diff) | |
More docs for deps.
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 73b2e691..85264522 100644 --- a/README.exper +++ b/README.exper @@ -22,9 +22,15 @@ Current "experimental" features (use right-click on highlighted spans), also bound on C-M-up/C-M-down. -** Theorem dependencies: displaying and highlighting dependencies - Only works for Isabelle/classic at the moment. You must also - select the Isabelle option "Theorem Dependencies". +** Theorem dependencies: displaying and highlighting dependencies. + Dependencies (e.g. lemmas) for a theorem are highlighted in + yellow, places where the theorem is used are highlighted + in orange. This allows easy editing of theories to remove + dead lemmas, re-order proofs, etc. + + Only works for Isabelle/classic at the moment (support is + required from proof assistant authors: please mention to them). + You must also select the Isabelle option "Theorem Dependencies". |