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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
