Re: [isabelle] Isabelle2015-RC0 available for testing



On 13.04.2015 15:06, Lars Noschinski wrote:
> 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:
This is documented in the NEWS file, but the error message is still
irritating.
> 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).





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