[isabelle-dev] Nominal and FinFuns from the AFP
andreas.lochbihler at kit.edu
Thu May 31 13:23:16 CEST 2012
> 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
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.
Karlsruher Institut für Technologie
Am Fasanengarten 5, Geb. 50.34, Raum 025
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
in der Helmholtz-Gemeinschaft
More information about the isabelle-dev