Changes between Initial Version and Version 1 of Ticket #307


Ignore:
Timestamp:
Nov 30, 2009, 11:48:03 PM (14 years ago)
Author:
David Aspinall
Comment:

Many thanks for the useful test case and explanation. Fixed now in proof-script 10.58: the undo is not allowed while processing is active, you get the "Proof Shell Busy" message.

Legend:

Unmodified
Added
Removed
Modified

  • Ticket #307

    • Property Status changed from new to closed
    • Property Resolution changed from to fixed

  • Ticket #307 – Description

    initial v1  
    22
    331. load the following script, which contains a nonterminating  command:
    4 
     4{{{
    55  theory Scratch imports Main begin
    66
    … …  
    99  lemma "P (Suc x)"
    1010  apply (simp add: foo)
    11 
     11}}}
    12122. Go to the simp-command that does not terminate
    1313