diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..22d0050 --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +output + diff --git a/Core_DOM/Core_DOM/ROOT b/Core_DOM/Core_DOM/ROOT index 7cceaab..65fc181 100644 --- a/Core_DOM/Core_DOM/ROOT +++ b/Core_DOM/Core_DOM/ROOT @@ -1,7 +1,7 @@ chapter AFP session "Core_DOM" (AFP) = "HOL-Library" + - options [timeout = 1200] + options [timeout = 1200, document = pdf, document_variants="document:outline=/proof,/ML",document_output=output] directories "common" "common/classes" @@ -18,3 +18,4 @@ session "Core_DOM" (AFP) = "HOL-Library" + document_files (in "document") "root.tex" "root.bib" + diff --git a/Core_DOM/Core_SC_DOM/ROOT b/Core_DOM/Core_SC_DOM/ROOT index 4b337e3..b9ba03f 100644 --- a/Core_DOM/Core_SC_DOM/ROOT +++ b/Core_DOM/Core_SC_DOM/ROOT @@ -1,7 +1,7 @@ chapter AFP session "Core_SC_DOM" (AFP) = "HOL-Library" + - options [timeout = 1200] + options [timeout = 1200, document = pdf, document_variants="document:outline=/proof,/ML",document_output=output] directories "common" "common/classes"