Re: [isabelle] AFP Incompleteness Entry
> It's certainly possible, and it seems that was indeed the issue. Using
> the HOL heap instead of HOL-Library yields success for me. Perhaps this
> caveat should be mentioned on the AFP site? It seems like the root of
> the issue here is some difference with multiset (at least, the first
> error I got in Nominal2_Base was the instance of multiset :: (pt) pt).
it is already documented in some way: the ROOT file specifies the parent
session. In case of "Incompleteness":
session Incompleteness (AFP) = HOL +
But it is true that it could be clarified in general.
This archive was generated by a fusion of
Pipermail (Mailman edition) and