[isabelle-dev] Declaration depending on user proofs

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Wed Nov 3 08:58:52 CET 2010

> So what are the "aesthetic and technical reasons" here?

Well, already some time ago I had the impression that there is a fear of
keyword number explosion.  Personally, I indeed don't care much.

Of course the Ā»globalĀ« nature of keywords makes it difficult to do
ad-hoc experimentation with new keywords, one generic slot would
simplify this.  Again, this is no pressing issue.

So, the suggestion seems to be to go ahead with new keywords.




PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20101103/69a2fa90/attachment.sig>

More information about the isabelle-dev mailing list