[isabelle-dev] Checked "assume" command

[Christian Urban]

On Wednesday, September 5, 2012 at 13:24:27 (+0200), Makarius wrote:
 > On Tue, 4 Sep 2012, Lars Noschinski wrote:
 > 
 > > As an user, an easy method to test whether the current set of 
 > > assumptions still fit one of the pending goals is "fix P show P sorry". 
 > > As I don't know any scenario where wrong assumptions would have an 
 > > useful effect, I propose to embed this check into the assume command.
 > 
 > I did not know the "fix P show P sorry" trick yet, but this is something 
 > for isabelle-users.
 > 
 > Generally, any changes to the core of the Isar proof engine (proof.ML) are 
 > restricted to exactly one person: myself.  

... or in the words of another famous Frenchman:

  "L'état, c'est moi"


Sorry, could not resist this spam email ;o)

Christian

 > This policy stems from the 
 > experience over the years, and people trying to tinker with its very 
 > delicate balance of how things work.  It takes myself often years of 
 > rethinking and reforming some of its fundamental details that emerged so 
 > well in the pionerring years of 1999-2001.
 > 
 > BTW, it is part of the classic Isar principles that assumptions alone 
 > cannot be "wrong", and there is a-priori no goal focus for results.
 > 
 > 
 > In recent years some side conditions of Isar have changed anyway: with the 
 > advent of the Prover IDE, system feedback is no longer restricted to the 
 > peepwhole view of a single command with its associated proof state. 
 > There can be additional feedback with knowledge of the partial proof 
 > document and its structure that is already in the editor buffer.
 > 
 > I have already started some very small beginnings there, to make the 
 > editing experience of Isar proofs fit into the PIDE mode, mainly about the 
 > ending of proofs so far.
 > 
 > This will require much more work.  What helps most are observations from 
 > practice what works smoothly and what not, without any specific proposals 
 > how the Isar machinery should be changed.
 > 
 > 
 >  	Makarius
 > _______________________________________________
 > isabelle-dev mailing list
 > isabelle-dev at in.tum.de
 > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

--