[isabelle-dev] Future of permanent_interpretation

Clemens Ballarin ballarin at in.tum.de
Mon Nov 9 20:58:24 CET 2015

 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.


More information about the isabelle-dev mailing list