[isabelle-dev] Interpretation with definitions [was Locale interpretation with mixins]

[Clemens Ballarin]

Hi Florian,

> Anyway, I am not so much concerned about syntax.  My primary intention
> is to get rid of the experimental code in interpretation_with_defs.ML,
> according to the following agenda:
> a) Decide for a particular syntax (at the moment this can only be (*) as
> it is conservative)
> b) Enhance »interpretation« accordingly.  Also a different command can
> be considered, but the interfaces in expression.ML must be extended in
> any case.

If you must do this, please provide a separate command, don't just  
modify 'interpretation'.  Generalisation of 'interpretation' to locale  
targets as a light-weight variant to 'sublocale' is still on the  
roadmap (although without a concrete date) and I would like to avoid  
additional complications here.  Also, I've worked hard for  
'interpretation', 'interpret' and 'sublocale' to have uniform syntax,  
and I would like this to remain so.

Eventually, we will need to follow the route suggested by Makarius in  
the other fork of this thread, so local definitions behave properly in  
tools like the simplifier.

Clemens