Opened 17 years ago
Closed 17 years ago
#115 closed enhancement (fixed)
Isabelle find-theorems form
| Reported by: | David Aspinall | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | PG-Emacs-3.7 |
| Component: | 2:pg-emacs | Keywords: | |
| Cc: |
Description (last modified by )
Contribution from Tjark Weber:
We have a tested and (hopefully) stable version of the search form now, that I think is ready to be integrated with the CVS version of ProofGeneral.
I don't have write access to the CVS repository, so I'm sending the files to you instead. The attached archive contains two files: ProofGeneral/isar/isar.el and ProofGeneral/isar/find-theorems.el. The latter is new, while only a few lines of the former have been modified to integrate the search form.
Please let me know what you think. (Feel free to take a look at the code and improve it if you like, of course.)
Attachments (2)
Change History (5)
Changed 17 years ago by
Changed 17 years ago by
| Attachment: | find-theorems.el added |
|---|
comment:1 Changed 17 years ago by
| Description: | modified (diff) |
|---|---|
| Status: | new → assigned |
comment:2 Changed 17 years ago by
| Description: | modified (diff) |
|---|
comment:3 Changed 17 years ago by
| Resolution: | → fixed |
|---|---|
| Status: | assigned → closed |
Note: See
TracTickets for help on using
tickets.
Status: I have added this to CVS head, but it doesn't work on XEmacs 21.5:
Seems to work OK on GNU Emacs 21.4.1, although lots of beeps on field validation (Emacs effect?).
Useful improvement would be to highlight the theorem names in the output so they can be automatically inserted back into the proof script, or even generate proof commands. Code to do this is already available.