[isabelle-dev] Checked "assume" command

[Makarius]

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