[isabelle-dev] "set_comprehension_pointfree" simproc losing bounds
makarius at sketis.net
Wed Oct 17 14:25:10 CEST 2012
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.
More information about the isabelle-dev