Am 05/09/2012 15:46, schrieb 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.
I don't understand this empirical approach and the IDE angle. You don't dispute that the proofs that Lars' check rejects cannot be completed without modifying the assumption in question? So what is the potential gain of not telling the user about it? Over the past decade I have frequently been in this situation and have always regarded the absence of such a check as an annoyance. Tobias _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
