[isabelle-dev] HOL/Library/Code_Prolog.thy breakdown

[Makarius]

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