On Wed, 5 Sep 2012, Lars Noschinski wrote:
As far as I can see, the only way to issue a successful "show" after a
wrong assumption (or, if you prefer, an "assumption which does not fit
any of the pending goals") is discarding everything with "next". So, I
don't see anything useful which can be achived without the check, but
cannot with this check. If I just want to experiment, I can open another
block.
Also, this change gives an fail-early property, which is useful when
maintaining proofs.
Formally, I can just put this on my stack of things to be revisited
eventually.
What I need is to watch over the shoulders of more people trying to write
Isar proofs in the current Prover IDE. In May this year I had 15 people
and 2 days to get some impressions where to continue next.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
