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-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev