On Tue, 16 Oct 2012, Dmitriy Traytel wrote:
Fortunately, jedit treats a proof that used to work (but fails now due
to the above) as a sorry, such that I can continue working on whatever
follows in the theory until this issue is fixed.
This is a consequence of the parallel checking of terminal proof steps,
which is enabled by default for several weeks already: 'by' with some
failing method behaves like "by fail", although that is a bit different
from the "by `!!X. PROP X`" of 'sorry'.
In the next stage (not before the coming release) full sub-proofs shall be
treated in the same manner. Thus apart from convenient parallel checking,
the benefit will be some structural editing of nested proof texts.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
