[isabelle-dev] Nominal and FinFuns from the AFP

[Andreas Lochbihler]

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: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum 
in der Helmholtz-Gemeinschaft