[isabelle-dev] Nominal and FinFuns from the AFP

[Christian Urban]

Dear All,

In Nominal I am usually relying on types that are defined
in HOL or that I define myself. However, I now came across 
the FinFun development in the AFP by Andreas Lochbihler (thanks 
to Larry). The finfun type seems to be rather useful to Nominal 
users, since it has finite support, in contrast to the function 
type, which in general hasn't.

My question is how I should I interface with something that 
is in the AFP and with something that is (eventually) in the
distribution? The problem is that Nominal always needs a wrapper 
infrastructure for types, such as a definition of a permutation. 

How should I write this wrapper, especially what should the import 
paths be, so that users can conveniently use FinFuns and Nominal?

Should this wrapper be part of the AFP entry (in which case
the paths are clear, but then Nominal users have to fetch the
AFP explicitly and no Nominal example in the distribution can
depend on it)?

Or should the wrapper be part of Nominal (in which case I
can use it in examples, but I have no idea what the import
paths should be...the AFP can be anywhere)?

Or, should FinFun be part of the distribution (which would
make my life normal again)?

Is there any received wisdom for this problem?

Best wishes,
Christian