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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
