Hi Clemens, >> the story behind is not about syntax. It is really about the >> simultaneous definitions. For a motivation, you can have a look at the >> tutorial on code generation, section »Further issues«, »Locales and >> interpretation«, where the pattern behind interpretation plus definition >> is spelt out using the constant »funpows«. > > This looks to me like a special case, but maybe one that is encountered > frequently when generating code. What do you intend to do? Provide a > special version of interpretation for code generation?
the intension is:
def (in foo) bar where …
--[ interpretation foo: … ]-->
def (in -) bar where …
rather than
def (in foo) bar where …
--[ interpretation foo: … ]-->
abbreviation (in -) bar where …
with --[ … ]--> being the interpretation morphism. The interpretation +
defines pattern was something which could be accomplished rather simple,
so I decided to make an experimental start with this in December 2010.
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
