I am new to Isabelle proof assistant and want to use it to verify a standard proof of the Bruck Ryser Chowla theorem. Since this theorem is about symmetric block designs, I figured that the folder Design_Theory in Isabelle's Archive of Formal Proofs as well as other folders in the Archive would be useful for this.
So after downloading Isabelle, I decided to also download everything in its Archive of Formal Proofs. I placed all of these folders in the folder Isabelle2024/src/HOL, because there were already lots of other folders with proofs there. But when I did this, I noticed that although some of the downloaded *.thy files were successfully verified by Isabelle (no pink highlights), other *.thy files were not. For instance, Isabelle couldn't verify BIBD.thy as well as other files in Design_Theory. I traced this problem to the fact that the file Multisets_Extras.thy in Design_Theory imports files that are not in Design_Theory, so apparently Isabelle cannot find these files.
Does anybody know a way around this problem? Another way of phrasing my question might be, "Where is the best place within the Isabelle folders to download its Archive of Formal Proofs?"
Update: I found some help here: https://www.isa-afp.org/help/ I followed its instructions:
“If the AFP is in C:\afp, run the following command in a Cygwin terminal:
isabelle components -u /cygdrive/c/afp/thys“
but I haven’t tested it yet. Perhaps this is the answer.
