Formalisation in Isabelle/HOL of Schutz' axioms for Minkowski spacetime (and theorems of Chapter 3). This is intended to be exactly the same as is hosted on the AFP - however, the AFP version (found under this link: https://afp.theoremproving.org/entries/schutz_spacetime/) is not up-to-date yet.
Use isabelle build -D . from the folder schutz_spacetime to build the Isabelle session and generate the pdf. To send to the AFP, include the entire schutz_spacetime folder.