aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Makarius Wenzel <makarius@sketis.net>2007-06-13 22:48:06 +0000
committerGravatar Makarius Wenzel <makarius@sketis.net>2007-06-13 22:48:06 +0000
commit5ac089f4c1c169b44e231d82b9f3a12de5c1fa18 (patch)
treed9cd4b69c17e446cf1bc6ebdbb41ad943141224b /CHANGES
parent50e213462dc393e97b8b9bc70b94d78a1c22aca6 (diff)
added information about optional "Find Theorems" form;
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES12
1 files changed, 10 insertions, 2 deletions
diff --git a/CHANGES b/CHANGES
index 591e738c..59a6d144 100644
--- a/CHANGES
+++ b/CHANGES
@@ -42,14 +42,22 @@ Including numerous improvements from Stefan Monnier.
** Changes for Isabelle
-*** Support for Isabelle2005 and later development snapshots of Isabelle.
+*** Support for Isabelle2005 and later development snapshots of Isabelle 2007.
Additional menu functions and PGIP support for settings configuration
now controlled directly by Isabelle. Support for Unicode-safe
interaction (`proof-shell-unicode' variable).
Support for Isabelle2003 has been removed; results with Isabelle2004
-are not guaranteed. Code now works with PolyML 5 versions of Isabelle.
+are not guaranteed. Code now works with PolyML 5 versions of
+Isabelle.
+
+Optional search form for the "Find Theorems" command is available via
+C-c C-a C-f, the minibuffer interface is available via C-c C-a C-m.
+Variable proof-find-theorems-command (customizable via 'Proof-General
+-> Advanced -> Internals -> Prover Config') controls the default
+behavior of 'ProofGeneral -> Find Theorems' (C-c C-f): set to
+isar-find-theorems-form or isar-find-theorems-minibuffer.