On Thu, 13 Feb 2014, Dmitriy Traytel wrote:
So apart from some repairs of
src/HOL/Tools/Predicate_Compile/code_prolog.ML in a76c679c0218, the
changeset e42a3fc18458 makes more clear (in batch mode) that redefining
outer syntax commands is not supposed to happen. This provides a window
of opportunity to remove spurious redefinitions elsewhere, until the
coming release.
If nobody stops me, I will take care of
"~~/src/HOL/ex/Interpretations_with_Defs". It's redefinition of the
interpretation command disturbed me already for a while.
The main question here is to find a proper name for it. According to the
ancient code of honor in Isabelle development, the one who implements a
tool has the priority to devise a name for it.
I made Isabelle/Isar a very open platform many years ago, making it easy
to define new language elements on the spot. Freedom comes with the
responsible to abide to certain rules, and overriding commands is not
admissible, and never was. It is merely a historical accident that this
was not rejected more explicitly so far.
We used to have the same for the theorem name space in the past. It was
the same historical accident for the same technical reasons, but some
users thought it would be good to override existing names at will. That
lead to big confusion eventually, so after some years we could actually
engage in the efforts to clean up that aspect. Today it is hard to
imagine non-authentic theorem name space from the past, just like the
non-authentic syntax notation that was once common-place.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
