[isabelle-dev] Checked "assume" command
makarius at sketis.net
Wed Sep 5 13:53:46 CEST 2012
On Wed, 5 Sep 2012, Christian Urban wrote:
> 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)
Well, I am in this unfortunate situation that many of the things I did
over the years get used by many people.
But this is really in the danger of getting a SPAM thread now.
More information about the isabelle-dev