Formalization of IMO solutions in Isabelle/HOL
Step 0: (only once)
-
Folder IMO_files is made using Isabelle command: $ISABELLE_HOME/bin/isabelle mkroot IMO_files
-
The basic tex file for storing relevant information about the generated document: IMO_files/document/root.tex
Step 1:
- ROOT file saves the structure of the generated pdf file
Step 2:
- Adding (or changing) a new theory file in the folder IMO_files/solutions or IMO_files/statements
- Must be added in the ROOT file also
Step 3:
-
A pdf file is generated using Isabelle command: $ISABELLE_HOME/bin/isabelle build -D IMO_files
-
It is located at: IMO_files/output/document.pdf