[isabelle] AFP entries with the new imports system



AFP entries have been reformed to use the new imports system. For instance, in my entry Lp, the line

imports "HOL-Analysis.Analysis" "../Ergodic_Theory/SG_Library_Complement"

has been replaced with

imports "HOL-Analysis.Analysis" Ergodic_Theory.SG_Library_Complement

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)

Best,
Sebastien





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