summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

changeset 22965 | b81bbe298406 |

parent 22921 | 475ff421a6a3 |

child 22971 | a6812b6a36a5 |

1.1 --- a/NEWS Mon May 14 12:52:56 2007 +0200 1.2 +++ b/NEWS Mon May 14 13:24:22 2007 +0200 1.3 @@ -33,6 +33,13 @@ 1.4 1.5 * Command 'find_theorems': support "*" wildcard in "name:" criterion. 1.6 1.7 +* Proof General interface: A search form for the "Find Theorems" command is 1.8 +now available via C-c C-a C-f. The old minibuffer interface is available 1.9 +via C-c C-a C-m. Variable proof-find-theorems-command (customizable via 1.10 +'Proof-General -> Advanced -> Internals -> Prover Config') controls the 1.11 +default behavior of 'ProofGeneral -> Find Theorems' (C-c C-f): set to 1.12 +isar-find-theorems-form or isar-find-theorems-minibuffer. 1.13 + 1.14 * The ``prems limit'' option (cf. ProofContext.prems_limit) is now -1 1.15 by default, which means that "prems" (and also "fixed variables") are 1.16 suppressed from proof state output. Note that the ProofGeneral