Re: [isabelle] AFP Incompleteness Entry



Hi Corey,

> 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.

Cheers
Lars




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.