What is the conclusion of this thread for the coming release? Whatever
happens, the time window for it is approx. Nov/Dec 2015.
Historically, the 'permanent_interpretation' command had to stay outside
Isabelle/Pure and Main Isabelle/HOL, because it was overwriting the
'interpretation' command in an ad-hoc manner -- causing a lot of confusion
to everybody. (This incident also accelerated the strict discpline of
authentic commands.)
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.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
