[isabelle-dev] Future of permanent_interpretation

[Makarius]

What is the conclusion of this thread for the coming release? Whatever 
happens, the time window for it is approx. Nov/Dec 2015.

Historically, the 'permanent_interpretation' command had to stay outside 
Isabelle/Pure and Main Isabelle/HOL, because it was overwriting the 
'interpretation' command in an ad-hoc manner -- causing a lot of confusion 
to everybody.  (This incident also accelerated the strict discpline of 
authentic commands.)

It is formally trivial to have 'permanent_interpretation' in Isabelle/Pure 
as separate command. If there is a simple way to have just one 
'interpretation' command with 'defines' vs. 'rewrites', I would prefer 
that.


 	Makarius