--- a/src/Doc/ROOT Wed May 19 13:19:37 2021 +0200
+++ b/src/Doc/ROOT Wed May 19 13:21:08 2021 +0200
@@ -1,7 +1,7 @@
chapter Doc
session Classes (doc) in "Classes" = HOL +
- options [document_logo = "Isar", document_build = "build",
+ options [document_logo = "Isar", document_bibliography, document_build = "build",
document_variants = "classes", quick_and_dirty]
theories [document = false] Setup
theories Classes
@@ -18,7 +18,7 @@
"style.sty"
session Codegen (doc) in "Codegen" = HOL +
- options [document_logo = "Isar", document_build = "build",
+ options [document_logo = "Isar", document_bibliography, document_build = "build",
document_variants = "codegen", print_mode = "no_brackets,iff"]
sessions
"HOL-Library"
@@ -46,7 +46,7 @@
"style.sty"
session Corec (doc) in "Corec" = Datatypes +
- options [document_build = "build", document_variants = "corec"]
+ options [document_build = "build", document_bibliography, document_variants = "corec"]
theories
Corec
document_files (in "..")
@@ -62,7 +62,7 @@
"style.sty"
session Datatypes (doc) in "Datatypes" = HOL +
- options [document_build = "build", document_variants = "datatypes"]
+ options [document_build = "build", document_bibliography, document_variants = "datatypes"]
sessions
"HOL-Library"
theories [document = false]
@@ -82,7 +82,7 @@
"style.sty"
session Eisbach (doc) in "Eisbach" = HOL +
- options [document_logo = "Eisbach", document_build = "build",
+ options [document_logo = "Eisbach", document_bibliography, document_build = "build",
document_variants = "eisbach", quick_and_dirty,
print_mode = "no_brackets,iff", show_question_marks = false]
sessions
@@ -107,7 +107,7 @@
"style.sty"
session Functions (doc) in "Functions" = HOL +
- options [document_build = "build", document_variants = "functions",
+ options [document_build = "build", document_bibliography, document_variants = "functions",
skip_proofs = false, quick_and_dirty]
theories Functions
document_files (in "..")
@@ -134,7 +134,8 @@
"prelude.tex"
session Intro (doc) in "Intro" = Pure +
- options [document_logo = "_", document_build = "build", document_variants = "intro"]
+ options [document_logo = "_", document_bibliography, document_build = "build",
+ document_variants = "intro"]
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
@@ -150,7 +151,7 @@
"root.tex"
session Implementation (doc) in "Implementation" = HOL +
- options [document_logo = "Isar", document_build = "build",
+ options [document_logo = "Isar", document_bibliography, document_build = "build",
document_variants = "implementation", quick_and_dirty]
theories
Eq
@@ -179,8 +180,8 @@
"style.sty"
session Isar_Ref (doc) in "Isar_Ref" = HOL +
- options [document_logo = "Isar", document_build = "build", document_variants = "isar-ref",
- quick_and_dirty, thy_output_source]
+ options [document_logo = "Isar", document_bibliography, document_build = "build",
+ document_variants = "isar-ref", quick_and_dirty, thy_output_source]
sessions
"HOL-Library"
theories
@@ -215,7 +216,7 @@
"style.sty"
session JEdit (doc) in "JEdit" = HOL +
- options [document_logo = "jEdit", document_build = "build",
+ options [document_logo = "jEdit", document_bibliography, document_build = "build",
document_variants = "jedit", thy_output_source]
theories
JEdit
@@ -253,7 +254,7 @@
"theories.png"
session Sugar (doc) in "Sugar" = HOL +
- options [document_build = "build", document_variants = "sugar"]
+ options [document_build = "build", document_bibliography, document_variants = "sugar"]
sessions
"HOL-Library"
theories Sugar
@@ -266,8 +267,8 @@
"root.tex"
session Locales (doc) in "Locales" = HOL +
- options [document_build = "build", document_variants = "locales",
- thy_output_margin = 65, skip_proofs = false]
+ options [document_build = "build", document_bibliography,
+ document_variants = "locales", thy_output_margin = 65, skip_proofs = false]
theories
Examples1
Examples2
@@ -281,7 +282,8 @@
"root.tex"
session Logics (doc) in "Logics" = Pure +
- options [document_logo = "_", document_build = "build", document_variants = "logics"]
+ options [document_logo = "_", document_bibliography, document_build = "build",
+ document_variants = "logics"]
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
@@ -300,7 +302,7 @@
"syntax.tex"
session Logics_ZF (doc) in "Logics_ZF" = ZF +
- options [document_logo = "ZF", document_build = "build",
+ options [document_logo = "ZF", document_bibliography, document_build = "build",
document_variants = "logics-ZF", print_mode = "brackets", thy_output_source]
sessions
FOL
@@ -334,7 +336,8 @@
"root.tex"
session Nitpick (doc) in "Nitpick" = Pure +
- options [document_logo = "Nitpick", document_build = "build", document_variants = "nitpick"]
+ options [document_logo = "Nitpick", document_bibliography, document_build = "build",
+ document_variants = "nitpick"]
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
@@ -345,7 +348,7 @@
"root.tex"
session Prog_Prove (doc) in "Prog_Prove" = HOL +
- options [document_logo = "HOL", document_build = "build",
+ options [document_logo = "HOL", document_bibliography, document_build = "build",
document_variants = "prog-prove", show_question_marks = false]
theories
Basics
@@ -369,7 +372,8 @@
"svmono.cls"
session Sledgehammer (doc) in "Sledgehammer" = Pure +
- options [document_logo = "S/H", document_build = "build", document_variants = "sledgehammer"]
+ options [document_logo = "S/H", document_bibliography, document_build = "build",
+ document_variants = "sledgehammer"]
document_files (in "..")
"prepare_document"
"pdfsetup.sty"
@@ -380,7 +384,7 @@
"root.tex"
session System (doc) in "System" = Pure +
- options [document_logo = "_", document_build = "build",
+ options [document_logo = "_", document_bibliography, document_build = "build",
document_variants = "system", thy_output_source]
sessions
"HOL-Library"
@@ -408,7 +412,7 @@
"root.tex"
session Tutorial (doc) in "Tutorial" = HOL +
- options [document_logo = "HOL", document_build = "build",
+ options [document_logo = "HOL", document_bibliography, document_build = "build",
document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
directories "Advanced" "CTL" "CodeGen" "Datatype" "Documents" "Fun" "Ifexpr"
"Inductive" "Misc" "Protocol" "Rules" "Sets" "ToyList" "Trie" "Types"
@@ -502,7 +506,7 @@
"types0.tex"
session Typeclass_Hierarchy (doc) in "Typeclass_Hierarchy" = HOL +
- options [document_logo = "Isar", document_build = "build",
+ options [document_logo = "Isar", document_bibliography, document_build = "build",
document_variants = "typeclass_hierarchy"]
sessions
"HOL-Library"