[isabelle-dev] Checked "assume" command
makarius at sketis.net
Wed Sep 5 15:46:13 CEST 2012
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
> 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
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.
More information about the isabelle-dev