[isabelle-dev] HOL/Library/Code_Prolog.thy breakdown
makarius at sketis.net
Thu Feb 13 20:00:08 CET 2014
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.
More information about the isabelle-dev