[isabelle-dev] Checked "assume" command

[Makarius]

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.


 	Makarius