[isabelle-dev] Fwd: A possible bug with Isabelle 2013
makarius at sketis.net
Wed Feb 27 16:38:05 CET 2013
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.
More information about the isabelle-dev