[isabelle-dev] Nominal and FinFuns from the AFP

[Andreas Lochbihler]

Dear Lukas and Christian,

> Or, should FinFun be part of the distribution (which would
> make my life normal again)?
When I submitted FinFun to the AFP, Tobias, Florian and I have already discussed 
whether FinFun should go to the AFP or HOL/Library. We decided in favour of AFP 
because I kept full access to continue the formalisation and nothing in the 
distribution depended on FinFuns. Now, matters are different and -- as Lukas has 
pointed out -- I now have write access to the Isabelle distribution, so there 
are no reasons for not moving it to the AFP.

Moreover, Gerwin can then finally test the subsumed marker of the AFP ;-)

Who is going to move the entry?

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