[isabelle-dev] "set_comprehension_pointfree" simproc losing bounds

[Makarius]

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