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)

Second_Steps.thy (493 bytes) - added by nils 14 years ago.

Download all attachments as: .zip

Change History (4)

Changed 14 years ago by nils

Attachment: Second_Steps.thy added

comment:1 in reply to:  description Changed 14 years ago by nils

my version: Proof General Eclipse 1.0.6.201007051138

comment:2 Changed 14 years ago by David Aspinall

Component: 2:pg-emacs1:pg-eclipse
Milestone: PG-Emacs-4.0PG-Eclipse-1.0.6

Thanks for the report. Will investigate soon.

comment:3 Changed 11 years ago by David Aspinall

Milestone: PG-Eclipse-1.0.6

Milestone PG-Eclipse-1.0.6 deleted

Note: See TracTickets for help on using tickets.