[isabelle-dev] Fwd: A possible bug with Isabelle 2013

[Makarius]

On Wed, 27 Feb 2013, Lawrence Paulson wrote:

> To me it hardly differs from "Fails to refine any pending goal", and it 
> should be treated similarly.

This feature actually has caused a lot of trouble over the years.  Just 
for Isabelle2013, I had to repair the error-side-exit once again, after it 
was broken by accident.

The pre-warning of 'show' potentially failing was never a real solution in 
the first place.  In the next round of refining the interactive checking 
of Isar proofs, it might be ultimately replaced by somthing that observes 
the block structure properly.


 	Makarius