[isabelle-dev] Future of permanent_interpretation

[Clemens Ballarin]

 On 09 November, 2015 11:56 CET, Makarius <makarius at sketis.net> wrote: 
 
> 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.

I would prefer to just have 'interpretation' as well.  Possibly 'sublocale' should also be extended by a 'defines' clause.

Clemens