Re: [isabelle] AFP entries with the new imports system



Dear Sebastien,

> and I understand this is the way to go. However, I did not find
> documentation explaining how to setup Isabelle so that
> Ergodic_Theory.SG_Library_Complement is correctly found on my computer
> (it currently gives me Bad theory import
> "Ergodic_Theory.SG_Library_Complement"). Is there a pointer to
> up-to-date documentation regarding this? (for instance,
> https://www.isa-afp.org/using.html is outdated in this respect)

see
<https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2017-August/msg00053.html>
for the two choices you have.

Cheers
Lars




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