Re: [isabelle] Isabelle2015-RC0 available for testing



On 11.04.2015 21:49, Makarius wrote:
> Any problems, observations etc. can be discussed here on the mailing
> list. Quite often a change of behaviour is perceived as a problem, and
> sometimes it is one, sometimes not.  In any case, open discussion
> helps to figure out what is potentially confusing to users.
I just noticed that oops does not work in a notepad:

theory Scratch imports Main begin

notepad begin
  have False
    oops

The oops fails with the following error message:

    Illegal application of command "oops"â in proof mode

I find this error message irritating (because usually oops works just
fine in proof mode). Also, I would like to use oops in notepads to mark
failed proof attempts (in contrast to incomplete ones, where I would use
sorry).

  -- Lars




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.