[isabelle-dev] Nominal and FinFuns from the AFP

Andreas Lochbihler andreas.lochbihler at kit.edu
Thu May 31 13:23:16 CEST 2012

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 
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
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
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum 
in der Helmholtz-Gemeinschaft

More information about the isabelle-dev mailing list