From 5ac089f4c1c169b44e231d82b9f3a12de5c1fa18 Mon Sep 17 00:00:00 2001 From: Makarius Wenzel Date: Wed, 13 Jun 2007 22:48:06 +0000 Subject: added information about optional "Find Theorems" form; --- CHANGES | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) (limited to 'CHANGES') 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. -- cgit v1.2.3