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_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
