1

Using Isabelle and the theories LaTeXsugar OptionalSugar Archimedean_Field where the latex documentation block contain

text " ... @{class floor_ceiling} ... "

when running isabelle build -d . S the process fail. The file ROOT contain

session "S" = "HOL" +
options [document = pdf, document_output = "generated"]
theories
 S
document_files
 build.sh

where the wiki direction of was followed.

Johan
  • 575
  • 5
  • 21

1 Answers1

0

The solution was to make the document class a book int he file root.tex: \documentclass[11pt,a4paper]{book}

The source of the error was chapter "Type definition in the thy file.

Johan
  • 575
  • 5
  • 21