[isabelle-dev] smt2

[Jasmin Blanchette]

Hi Andreas,

>> How big an issue is it to you if we move narrowing to Library?
> [...] If you do so, please make sure that the connection to the datatype packages is kept, i.e., narrowing generators are generated for all datatypes (even those that are defined while narrowing was not in scope).

This happens automatically for all datatype extensions (or "interpretations" as they are officially called). This is how "bool", "sum", "prod", and "nat" get their "size" functions, even though "size" is registered much later.

> IIRC, the AFP policy is (was?) that all entries that import at least one theory from HOL-Library are based on HOL-Library.

(I presume if you pull things from various unrelated sources (say, "Multivariate_Analysis" and "Library"), you have the choice.)

Jasmin