summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | webertj |

Mon, 14 May 2007 13:24:22 +0200 | |

changeset 22965 | b81bbe298406 |

parent 22964 | 2284e0d02e7f |

child 22966 | 9dc4f5048353 |

ProofGeneral: Find Theorems search form

--- a/NEWS Mon May 14 12:52:56 2007 +0200 +++ b/NEWS Mon May 14 13:24:22 2007 +0200 @@ -33,6 +33,13 @@ * Command 'find_theorems': support "*" wildcard in "name:" criterion. +* Proof General interface: A search form for the "Find Theorems" command is +now available via C-c C-a C-f. The old 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. + * The ``prems limit'' option (cf. ProofContext.prems_limit) is now -1 by default, which means that "prems" (and also "fixed variables") are suppressed from proof state output. Note that the ProofGeneral