Opened 14 years ago
Last modified 11 years ago
#353 new defect
"undo last proof command" does not work at the end of theory
Reported by: | nils | Owned by: | David Aspinall |
---|---|---|---|
Priority: | major | Milestone: | |
Component: | 1:pg-eclipse | Keywords: | |
Cc: |
Description
there are only ML commands in this theory, and when it is processed until the final end, the undo proof command does not work anymore.
Attachments (1)
Change History (4)
Changed 14 years ago by
Attachment: | Second_Steps.thy added |
---|
comment:1 Changed 14 years ago by
comment:2 Changed 14 years ago by
Component: | 2:pg-emacs → 1:pg-eclipse |
---|---|
Milestone: | PG-Emacs-4.0 → PG-Eclipse-1.0.6 |
Thanks for the report. Will investigate soon.
Note: See
TracTickets for help on using
tickets.
my version: Proof General Eclipse 1.0.6.201007051138