On 09 November, 2015 11:56 CET, Makarius <makar...@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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
