From 60a84ffa180c02e7d78fadada20b58a238319bbf Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 8 Aug 2002 12:17:14 +0000 Subject: More docs for deps. --- README.exper | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) (limited to 'README.exper') 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". -- cgit v1.2.3