Hi all, > > In the short term, we could move the FinFun theory into the HOL library > > of the development version after Isabelle 2012 and the AFP 2012 has been > > released, if we agree that this moves this contribution in the right > > direction.
some remarks on my behalf:
a) Ideally, tools and library theories span a product space: tools
should provide configuration means such that theories »not forseen by
the author« can be integrated into its scope, typically by a series of
declarations. AFP library theories are a nice case study for this – if
the AFP infrastructure would not allow for such organization
(dependencies etc.), it does not fullfil its promise.
b) In the particular case of FinFun, more and more tools seem to regard
this as so fundamental (or fundamentally helpful) that incorporation
into the distribution could indeed be the answer. Nevertheless, I would
like to see explicit statements on this.
For the moment, we have a claim for Nominal. I want to add that I would
like to see a type for executable mappings in the distribution, and
FinFuns seems to be the most reasonable candidate. More claims?
c) I strongly object to clutter the HOL syntax even more than now by
incorporating just another fancy syntax. I would prefer the lattice
solution (delete syntax immediately after use and provide a library
theory to optionally include it later), or maybe it is also possible to
use context blocks for this (another nice case study).
d) In personal conversation Alex and I discussed whether it would be
preferable to swap FinFun.thy into HOL-Main and Map.thy into
HOL-Library, but I don't recall the arguments in particular.
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
