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: [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
