[isabelle-dev] Interpretation with definitions [was Locale interpretation with mixins]
ballarin at in.tum.de
Sat Sep 8 20:52:50 CEST 2012
> 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.
More information about the isabelle-dev