Hi Makarius,
At some point, when I have bundles ready to work with the existing
notation commands, we can fine-tune this scheme further, to allow users to
'include' syntax in local situations.
I tried to implement the new syntax for FinFuns with bundles and Brian's
notation attribute
(https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2012-April/002585.html),
but it was not satisfactory.
There were two show stoppers:
1. I did not know how to get dynamic bundles, i.e., how to add declarations one
after the other to a bundle. Hence, I would have to introduce all the notation
in a single place before which all constants must have been defined.
2. Theory-level commands like interpretation do not work inside an auxiliary
context and neither can they cope wth "includes". Hence, I cannot use such
pretty syntax in the parameter instantiations for interpretation. This possibly
also applies to the where clause although I did not need that for FinFun.
Andreas
--
Karlsruher Institut für Technologie
IPD Snelting
Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: [email protected]
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
in der Helmholtz-Gemeinschaft
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
