I would like to obtain the LaTeX code associated with this theory. Previous answers only provide links to the documentation. Let me describe what I did.
I went to the directory of Hales.thy
and executed isabelle mkroot
, followed by isabelle build -D .
, which generated a file named document and a *.pdf
file which was suspiciously (nearly) empty. Modifications of this command by adding Hales.thy
as a parameter didn't succeed.
I would appreciate if someone could describe briefly the commands needed.