[isabelle-dev] Future of permanent_interpretation

Makarius makarius at sketis.net
Mon Nov 9 11:56:04 CET 2015

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 


More information about the isabelle-dev mailing list