[isabelle-dev] Declaration depending on user proofs
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev