| author | wenzelm | 
| Mon, 23 Dec 2019 22:35:54 +0100 | |
| changeset 71344 | ee9998bb417b | 
| parent 71099 | 20c1b9516d27 | 
| child 71893 | a27747c85700 | 
| permissions | -rw-r--r-- | 
| 51397 
03b586ee5930
support for 'chapter' specifications within session ROOT;
 wenzelm parents: 
50426diff
changeset | 1 | chapter Doc | 
| 
03b586ee5930
support for 'chapter' specifications within session ROOT;
 wenzelm parents: 
50426diff
changeset | 2 | |
| 48950 
9965099f51ad
more standard document preparation within session context;
 wenzelm parents: 
48949diff
changeset | 3 | session Classes (doc) in "Classes" = HOL + | 
| 55385 
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
 wenzelm parents: 
55159diff
changeset | 4 | options [document_variants = "classes", quick_and_dirty] | 
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 5 | theories [document = false] Setup | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 6 | theories Classes | 
| 56534 | 7 | document_files (in "..") | 
| 8 | "prepare_document" | |
| 9 | "pdfsetup.sty" | |
| 10 | "iman.sty" | |
| 11 | "extra.sty" | |
| 12 | "isar.sty" | |
| 13 | "manual.bib" | |
| 14 | document_files | |
| 15 | "build" | |
| 16 | "root.tex" | |
| 17 | "style.sty" | |
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 18 | |
| 69422 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 19 | session Codegen (doc) in "Codegen" = HOL + | 
| 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 20 | options [document_variants = "codegen", print_mode = "no_brackets,iff"] | 
| 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 21 | sessions | 
| 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 22 | "HOL-Library" | 
| 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 23 | theories [document = false] | 
| 59378 
065f349852e6
separate image for prerequisites of codegen tutorial
 haftmann parents: 
59175diff
changeset | 24 | Setup | 
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 25 | theories | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 26 | Introduction | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 27 | Foundations | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 28 | Refinement | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 29 | Inductive_Predicate | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 30 | Evaluation | 
| 65041 | 31 | Computations | 
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 32 | Adaptation | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 33 | Further | 
| 56534 | 34 | document_files (in "..") | 
| 35 | "prepare_document" | |
| 36 | "pdfsetup.sty" | |
| 37 | "iman.sty" | |
| 38 | "extra.sty" | |
| 39 | "isar.sty" | |
| 40 | "manual.bib" | |
| 41 | document_files | |
| 42 | "build" | |
| 43 | "root.tex" | |
| 44 | "style.sty" | |
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 45 | |
| 69422 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 46 | session Corec (doc) in "Corec" = Datatypes + | 
| 62739 | 47 | options [document_variants = "corec"] | 
| 69422 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 48 | theories | 
| 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 49 | Corec | 
| 62739 | 50 | document_files (in "..") | 
| 51 | "prepare_document" | |
| 52 | "pdfsetup.sty" | |
| 53 | "iman.sty" | |
| 54 | "extra.sty" | |
| 55 | "isar.sty" | |
| 56 | "manual.bib" | |
| 57 | document_files | |
| 58 | "build" | |
| 59 | "root.tex" | |
| 60 | "style.sty" | |
| 61 | ||
| 69422 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 62 | session Datatypes (doc) in "Datatypes" = HOL + | 
| 53618 | 63 | options [document_variants = "datatypes"] | 
| 69422 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 64 | sessions | 
| 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 65 | "HOL-Library" | 
| 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 66 | theories [document = false] | 
| 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 67 | Setup | 
| 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 68 | theories | 
| 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 69 | Datatypes | 
| 56534 | 70 | document_files (in "..") | 
| 71 | "prepare_document" | |
| 72 | "pdfsetup.sty" | |
| 73 | "iman.sty" | |
| 74 | "extra.sty" | |
| 75 | "isar.sty" | |
| 76 | "manual.bib" | |
| 77 | document_files | |
| 78 | "build" | |
| 79 | "root.tex" | |
| 80 | "style.sty" | |
| 52792 
3e651be14fcd
sketched documentation for new (co)datatype package
 blanchet parents: 
52742diff
changeset | 81 | |
| 69422 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 82 | session Eisbach (doc) in "Eisbach" = HOL + | 
| 60288 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 83 | options [document_variants = "eisbach", quick_and_dirty, | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 84 | print_mode = "no_brackets,iff", show_question_marks = false] | 
| 69422 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 85 | sessions | 
| 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 86 | "HOL-Eisbach" | 
| 60288 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 87 | theories [document = false] | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 88 | Base | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 89 | theories | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 90 | Preface | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 91 | Manual | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 92 | document_files (in "..") | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 93 | "prepare_document" | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 94 | "pdfsetup.sty" | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 95 | "iman.sty" | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 96 | "extra.sty" | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 97 | "isar.sty" | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 98 | "ttbox.sty" | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 99 | "underscore.sty" | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 100 | "manual.bib" | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 101 | document_files | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 102 | "build" | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 103 | "root.tex" | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 104 | "style.sty" | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 105 | |
| 48948 
fa49f8890ef3
more standard document preparation within session context;
 wenzelm parents: 
48947diff
changeset | 106 | session Functions (doc) in "Functions" = HOL + | 
| 54017 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
 krauss parents: 
53769diff
changeset | 107 | options [document_variants = "functions", skip_proofs = false, quick_and_dirty] | 
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 108 | theories Functions | 
| 56534 | 109 | document_files (in "..") | 
| 110 | "prepare_document" | |
| 111 | "pdfsetup.sty" | |
| 112 | "iman.sty" | |
| 113 | "extra.sty" | |
| 114 | "isar.sty" | |
| 115 | "manual.bib" | |
| 116 | document_files | |
| 117 | "build" | |
| 118 | "conclusion.tex" | |
| 119 | "intro.tex" | |
| 120 | "mathpartir.sty" | |
| 121 | "root.tex" | |
| 122 | "style.sty" | |
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 123 | |
| 69105 
b7274dfbf4b3
explicit group "no_doc" for unfinished documentation, allows to suppress everything uniformly: -X doc -X no_doc;
 wenzelm parents: 
68677diff
changeset | 124 | session How_to_Prove_it (no_doc) in "How_to_Prove_it" = HOL + | 
| 56825 | 125 | options [document_variants = "how_to_prove_it", show_question_marks = false] | 
| 126 | theories | |
| 127 | How_to_Prove_it | |
| 128 | document_files | |
| 129 | "root.tex" | |
| 130 | "root.bib" | |
| 131 | "prelude.tex" | |
| 132 | ||
| 48969 | 133 | session Intro (doc) in "Intro" = Pure + | 
| 134 | options [document_variants = "intro"] | |
| 56534 | 135 | document_files (in "..") | 
| 136 | "prepare_document" | |
| 137 | "pdfsetup.sty" | |
| 138 | "iman.sty" | |
| 139 | "extra.sty" | |
| 140 | "ttbox.sty" | |
| 141 | "manual.bib" | |
| 142 | document_files | |
| 143 | "advanced.tex" | |
| 144 | "build" | |
| 145 | "foundations.tex" | |
| 146 | "getting.tex" | |
| 147 | "root.tex" | |
| 48969 | 148 | |
| 69422 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 149 | session Implementation (doc) in "Implementation" = HOL + | 
| 62354 | 150 | options [document_variants = "implementation", quick_and_dirty] | 
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 151 | theories | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 152 | Eq | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 153 | Integration | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 154 | Isar | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 155 | Local_Theory | 
| 67215 | 156 | "ML" | 
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 157 | Prelim | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 158 | Proof | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 159 | Syntax | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 160 | Tactic | 
| 52499 | 161 | theories [parallel_proofs = 0] | 
| 52410 | 162 | Logic | 
| 56534 | 163 | document_files (in "..") | 
| 164 | "prepare_document" | |
| 165 | "pdfsetup.sty" | |
| 166 | "iman.sty" | |
| 167 | "extra.sty" | |
| 168 | "isar.sty" | |
| 169 | "ttbox.sty" | |
| 170 | "underscore.sty" | |
| 171 | "manual.bib" | |
| 172 | document_files | |
| 173 | "build" | |
| 174 | "root.tex" | |
| 175 | "style.sty" | |
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 176 | |
| 69422 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 177 | session Isar_Ref (doc) in "Isar_Ref" = HOL + | 
| 48958 
12afbf6eb7f9
more standard document preparation within session context;
 wenzelm parents: 
48957diff
changeset | 178 | options [document_variants = "isar-ref", quick_and_dirty, thy_output_source] | 
| 69422 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 179 | sessions | 
| 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 180 | "HOL-Library" | 
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 181 | theories | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 182 | Preface | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 183 | Synopsis | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 184 | Framework | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 185 | First_Order_Logic | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 186 | Outer_Syntax | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 187 | Document_Preparation | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 188 | Spec | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 189 | Proof | 
| 60484 | 190 | Proof_Script | 
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 191 | Inner_Syntax | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 192 | Generic | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 193 | HOL_Specific | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 194 | Quick_Reference | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 195 | Symbols | 
| 56534 | 196 | document_files (in "..") | 
| 197 | "prepare_document" | |
| 198 | "pdfsetup.sty" | |
| 199 | "iman.sty" | |
| 200 | "extra.sty" | |
| 201 | "isar.sty" | |
| 202 | "ttbox.sty" | |
| 203 | "underscore.sty" | |
| 204 | "manual.bib" | |
| 205 | document_files | |
| 206 | "build" | |
| 207 | "isar-vm.pdf" | |
| 208 | "isar-vm.svg" | |
| 209 | "root.tex" | |
| 210 | "showsymbols" | |
| 211 | "style.sty" | |
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 212 | |
| 54354 | 213 | session JEdit (doc) in "JEdit" = HOL + | 
| 53769 | 214 | options [document_variants = "jedit", thy_output_source] | 
| 215 | theories | |
| 216 | JEdit | |
| 56534 | 217 | document_files (in "..") | 
| 218 | "extra.sty" | |
| 219 | "iman.sty" | |
| 220 | "isar.sty" | |
| 221 | "manual.bib" | |
| 222 | "pdfsetup.sty" | |
| 223 | "prepare_document" | |
| 224 | "ttbox.sty" | |
| 225 | "underscore.sty" | |
| 226 | document_files (in "../Isar_Ref/document") | |
| 227 | "style.sty" | |
| 228 | document_files | |
| 229 | "auto-tools.png" | |
| 60255 
0466bd194d74
more on Isabelle document preparation and bibtex files;
 wenzelm parents: 
59405diff
changeset | 230 | "bibtex-mode.png" | 
| 56534 | 231 | "build" | 
| 60255 
0466bd194d74
more on Isabelle document preparation and bibtex files;
 wenzelm parents: 
59405diff
changeset | 232 | "cite-completion.png" | 
| 62154 | 233 | "isabelle-jedit-hdpi.png" | 
| 56534 | 234 | "isabelle-jedit.png" | 
| 62154 | 235 | "markdown-document.png" | 
| 236 | "ml-debugger.png" | |
| 237 | "output-and-state.png" | |
| 238 | "output-including-state.png" | |
| 56534 | 239 | "output.png" | 
| 240 | "popup1.png" | |
| 241 | "popup2.png" | |
| 62154 | 242 | "query.png" | 
| 56534 | 243 | "root.tex" | 
| 64514 | 244 | "scope1.png" | 
| 245 | "scope2.png" | |
| 62154 | 246 | "sidekick-document.png" | 
| 57336 | 247 | "sidekick.png" | 
| 56534 | 248 | "sledgehammer.png" | 
| 57339 | 249 | "theories.png" | 
| 53769 | 250 | |
| 56420 
b266e7a86485
closer correspondence of document and session names, while maintaining document names for external reference
 haftmann parents: 
55385diff
changeset | 251 | session Sugar (doc) in "Sugar" = HOL + | 
| 48949 
a773af3e37d6
more standard document preparation within session context;
 wenzelm parents: 
48948diff
changeset | 252 | options [document_variants = "sugar"] | 
| 65573 
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
 wenzelm parents: 
65569diff
changeset | 253 | sessions | 
| 
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
 wenzelm parents: 
65569diff
changeset | 254 | "HOL-Library" | 
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 255 | theories Sugar | 
| 56534 | 256 | document_files (in "..") | 
| 257 | "prepare_document" | |
| 258 | "pdfsetup.sty" | |
| 259 | document_files | |
| 260 | "build" | |
| 261 | "mathpartir.sty" | |
| 262 | "root.bib" | |
| 263 | "root.tex" | |
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 264 | |
| 48943 
54da920baf38
more standard document preparation within session context;
 wenzelm parents: 
48942diff
changeset | 265 | session Locales (doc) in "Locales" = HOL + | 
| 59175 
bf465f335e85
system option "pretty_margin" is superseded by "thy_output_margin";
 wenzelm parents: 
58801diff
changeset | 266 | options [document_variants = "locales", thy_output_margin = 65, skip_proofs = false] | 
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 267 | theories | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 268 | Examples1 | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 269 | Examples2 | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 270 | Examples3 | 
| 56534 | 271 | document_files (in "..") | 
| 272 | "prepare_document" | |
| 273 | "pdfsetup.sty" | |
| 274 | document_files | |
| 275 | "build" | |
| 276 | "root.bib" | |
| 277 | "root.tex" | |
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 278 | |
| 48942 
75d8778f94d3
more standard document preparation within session context;
 wenzelm parents: 
48941diff
changeset | 279 | session Logics (doc) in "Logics" = Pure + | 
| 
75d8778f94d3
more standard document preparation within session context;
 wenzelm parents: 
48941diff
changeset | 280 | options [document_variants = "logics"] | 
| 56534 | 281 | document_files (in "..") | 
| 282 | "prepare_document" | |
| 283 | "pdfsetup.sty" | |
| 284 | "iman.sty" | |
| 285 | "extra.sty" | |
| 286 | "ttbox.sty" | |
| 287 | "manual.bib" | |
| 288 | document_files | |
| 289 | "CTT.tex" | |
| 290 | "HOL.tex" | |
| 291 | "LK.tex" | |
| 292 | "Sequents.tex" | |
| 293 | "build" | |
| 294 | "preface.tex" | |
| 295 | "root.tex" | |
| 296 | "syntax.tex" | |
| 48945 
b5758f5a469c
more standard document preparation within session context;
 wenzelm parents: 
48944diff
changeset | 297 | |
| 56451 
856492b0f755
even more standardized doc session names after #b266e7a86485
 haftmann parents: 
56420diff
changeset | 298 | session Logics_ZF (doc) in "Logics_ZF" = ZF + | 
| 48956 | 299 | options [document_variants = "logics-ZF", print_mode = "brackets", | 
| 300 | thy_output_source] | |
| 66444 | 301 | sessions | 
| 302 | FOL | |
| 48946 
a9b8344f5196
more standard document preparation within session context;
 wenzelm parents: 
48945diff
changeset | 303 | theories | 
| 
a9b8344f5196
more standard document preparation within session context;
 wenzelm parents: 
48945diff
changeset | 304 | IFOL_examples | 
| 
a9b8344f5196
more standard document preparation within session context;
 wenzelm parents: 
48945diff
changeset | 305 | FOL_examples | 
| 
a9b8344f5196
more standard document preparation within session context;
 wenzelm parents: 
48945diff
changeset | 306 | ZF_examples | 
| 
a9b8344f5196
more standard document preparation within session context;
 wenzelm parents: 
48945diff
changeset | 307 | If | 
| 48956 | 308 | ZF_Isar | 
| 56534 | 309 | document_files (in "..") | 
| 310 | "prepare_document" | |
| 311 | "pdfsetup.sty" | |
| 312 | "isar.sty" | |
| 313 | "ttbox.sty" | |
| 314 | "manual.bib" | |
| 315 | document_files (in "../Logics/document") | |
| 316 | "syntax.tex" | |
| 317 | document_files | |
| 318 | "FOL.tex" | |
| 319 | "ZF.tex" | |
| 320 | "build" | |
| 321 | "logics.sty" | |
| 322 | "root.tex" | |
| 48946 
a9b8344f5196
more standard document preparation within session context;
 wenzelm parents: 
48945diff
changeset | 323 | |
| 48944 
ac15a85e9282
more standard document preparation within session context;
 wenzelm parents: 
48943diff
changeset | 324 | session Main (doc) in "Main" = HOL + | 
| 
ac15a85e9282
more standard document preparation within session context;
 wenzelm parents: 
48943diff
changeset | 325 | options [document_variants = "main"] | 
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 326 | theories Main_Doc | 
| 56534 | 327 | document_files (in "..") | 
| 328 | "prepare_document" | |
| 329 | "pdfsetup.sty" | |
| 330 | document_files | |
| 331 | "build" | |
| 332 | "root.tex" | |
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 333 | |
| 48963 
f11d88bfa934
more standard document preparation within session context;
 wenzelm parents: 
48962diff
changeset | 334 | session Nitpick (doc) in "Nitpick" = Pure + | 
| 
f11d88bfa934
more standard document preparation within session context;
 wenzelm parents: 
48962diff
changeset | 335 | options [document_variants = "nitpick"] | 
| 56534 | 336 | document_files (in "..") | 
| 337 | "prepare_document" | |
| 338 | "pdfsetup.sty" | |
| 339 | "iman.sty" | |
| 340 | "manual.bib" | |
| 341 | document_files | |
| 342 | "build" | |
| 343 | "root.tex" | |
| 48963 
f11d88bfa934
more standard document preparation within session context;
 wenzelm parents: 
48962diff
changeset | 344 | |
| 56451 
856492b0f755
even more standardized doc session names after #b266e7a86485
 haftmann parents: 
56420diff
changeset | 345 | session Prog_Prove (doc) in "Prog_Prove" = HOL + | 
| 48947 
7eee8b2d2099
more standard document preparation within session context;
 wenzelm parents: 
48946diff
changeset | 346 | options [document_variants = "prog-prove", show_question_marks = false] | 
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 347 | theories | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 348 | Basics | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 349 | Bool_nat_list | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 350 | MyList | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 351 | Types_and_funs | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 352 | Logic | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 353 | Isar | 
| 56534 | 354 | document_files (in ".") | 
| 355 | "MyList.thy" | |
| 356 | document_files (in "..") | |
| 357 | "prepare_document" | |
| 358 | "pdfsetup.sty" | |
| 359 | document_files | |
| 360 | "bang.pdf" | |
| 361 | "build" | |
| 362 | "intro-isabelle.tex" | |
| 363 | "mathpartir.sty" | |
| 364 | "prelude.tex" | |
| 365 | "root.bib" | |
| 366 | "root.tex" | |
| 367 | "svmono.cls" | |
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 368 | |
| 48962 
a1acc1cb0271
more standard document preparation within session context;
 wenzelm parents: 
48961diff
changeset | 369 | session Sledgehammer (doc) in "Sledgehammer" = Pure + | 
| 
a1acc1cb0271
more standard document preparation within session context;
 wenzelm parents: 
48961diff
changeset | 370 | options [document_variants = "sledgehammer"] | 
| 56534 | 371 | document_files (in "..") | 
| 372 | "prepare_document" | |
| 373 | "pdfsetup.sty" | |
| 374 | "iman.sty" | |
| 375 | "manual.bib" | |
| 376 | document_files | |
| 377 | "build" | |
| 378 | "root.tex" | |
| 48962 
a1acc1cb0271
more standard document preparation within session context;
 wenzelm parents: 
48961diff
changeset | 379 | |
| 48937 
e7418f8d49fe
more standard document preparation within session context;
 wenzelm parents: 
48738diff
changeset | 380 | session System (doc) in "System" = Pure + | 
| 
e7418f8d49fe
more standard document preparation within session context;
 wenzelm parents: 
48738diff
changeset | 381 | options [document_variants = "system", thy_output_source] | 
| 67219 | 382 | sessions | 
| 383 | "HOL-Library" | |
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 384 | theories | 
| 62640 | 385 | Environment | 
| 48578 | 386 | Sessions | 
| 387 | Presentation | |
| 67904 | 388 | Server | 
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 389 | Scala | 
| 71099 
20c1b9516d27
documentation on Phabricator server administration;
 wenzelm parents: 
70678diff
changeset | 390 | Phabricator | 
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 391 | Misc | 
| 56534 | 392 | document_files (in "..") | 
| 393 | "prepare_document" | |
| 394 | "pdfsetup.sty" | |
| 395 | "iman.sty" | |
| 396 | "extra.sty" | |
| 397 | "isar.sty" | |
| 398 | "ttbox.sty" | |
| 399 | "underscore.sty" | |
| 400 | "manual.bib" | |
| 401 | document_files (in "../Isar_Ref/document") | |
| 402 | "style.sty" | |
| 403 | document_files | |
| 404 | "build" | |
| 405 | "root.tex" | |
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 406 | |
| 48985 | 407 | session Tutorial (doc) in "Tutorial" = HOL + | 
| 70678 
36c8c32346cb
clarified syntax: 'directories' and 'theories' belong together;
 wenzelm parents: 
70675diff
changeset | 408 | options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false] | 
| 70675 | 409 | directories "Advanced" "CTL" "CodeGen" "Datatype" "Documents" "Fun" "Ifexpr" | 
| 410 | "Inductive" "Misc" "Protocol" "Rules" "Sets" "ToyList" "Trie" "Types" | |
| 53376 | 411 | theories [threads = 1] | 
| 412 | "ToyList/ToyList_Test" | |
| 48526 | 413 | theories [thy_output_indent = 5] | 
| 414 | "ToyList/ToyList" | |
| 415 | "Ifexpr/Ifexpr" | |
| 416 | "CodeGen/CodeGen" | |
| 417 | "Trie/Trie" | |
| 418 | "Datatype/ABexpr" | |
| 419 | "Datatype/unfoldnested" | |
| 420 | "Datatype/Nested" | |
| 421 | "Datatype/Fundata" | |
| 422 | "Fun/fun0" | |
| 423 | "Advanced/simp2" | |
| 424 | "CTL/PDL" | |
| 425 | "CTL/CTL" | |
| 426 | "CTL/CTLind" | |
| 427 | "Inductive/Even" | |
| 428 | "Inductive/Mutual" | |
| 429 | "Inductive/Star" | |
| 430 | "Inductive/AB" | |
| 431 | "Inductive/Advanced" | |
| 432 | "Misc/Tree" | |
| 433 | "Misc/Tree2" | |
| 434 | "Misc/Plus" | |
| 435 | "Misc/case_exprs" | |
| 436 | "Misc/fakenat" | |
| 437 | "Misc/natsum" | |
| 438 | "Misc/pairs2" | |
| 439 | "Misc/Option2" | |
| 440 | "Misc/types" | |
| 441 | "Misc/prime_def" | |
| 442 | "Misc/simp" | |
| 443 | "Misc/Itrev" | |
| 444 | "Misc/AdvancedInd" | |
| 445 | "Misc/appendix" | |
| 446 | theories | |
| 447 | "Protocol/NS_Public" | |
| 448 | "Documents/Documents" | |
| 65573 
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
 wenzelm parents: 
65569diff
changeset | 449 | theories [document = false] | 
| 48526 | 450 | "Types/Setup" | 
| 59175 
bf465f335e85
system option "pretty_margin" is superseded by "thy_output_margin";
 wenzelm parents: 
58801diff
changeset | 451 | theories [thy_output_margin = 64, thy_output_indent = 0] | 
| 48526 | 452 | "Types/Numbers" | 
| 453 | "Types/Pairs" | |
| 454 | "Types/Records" | |
| 455 | "Types/Typedefs" | |
| 456 | "Types/Overloading" | |
| 457 | "Types/Axioms" | |
| 458 | "Rules/Basic" | |
| 459 | "Rules/Blast" | |
| 460 | "Rules/Force" | |
| 59175 
bf465f335e85
system option "pretty_margin" is superseded by "thy_output_margin";
 wenzelm parents: 
58801diff
changeset | 461 | theories [thy_output_margin = 64, thy_output_indent = 5] | 
| 55159 
608c157d743d
Replacing the theory Library/Binomial by Number_Theory/Binomial
 paulson <lp15@cam.ac.uk> parents: 
55073diff
changeset | 462 | "Rules/TPrimes" | 
| 48526 | 463 | "Rules/Forward" | 
| 464 | "Rules/Tacticals" | |
| 465 | "Rules/find2" | |
| 466 | "Sets/Examples" | |
| 467 | "Sets/Functions" | |
| 468 | "Sets/Relations" | |
| 469 | "Sets/Recur" | |
| 56534 | 470 | document_files (in "ToyList") | 
| 57083 | 471 | "ToyList1.txt" | 
| 472 | "ToyList2.txt" | |
| 56534 | 473 | document_files (in "..") | 
| 474 | "pdfsetup.sty" | |
| 475 | "ttbox.sty" | |
| 476 | "manual.bib" | |
| 477 | document_files | |
| 478 | "advanced0.tex" | |
| 479 | "appendix0.tex" | |
| 480 | "basics.tex" | |
| 481 | "build" | |
| 482 | "cl2emono-modified.sty" | |
| 483 | "ctl0.tex" | |
| 484 | "documents0.tex" | |
| 485 | "fp.tex" | |
| 486 | "inductive0.tex" | |
| 487 | "isa-index" | |
| 488 | "Isa-logics.pdf" | |
| 489 | "numerics.tex" | |
| 490 | "pghead.pdf" | |
| 491 | "preface.tex" | |
| 492 | "protocol.tex" | |
| 493 | "root.tex" | |
| 494 | "rules.tex" | |
| 495 | "sets.tex" | |
| 496 | "tutorial.sty" | |
| 497 | "typedef.pdf" | |
| 498 | "types0.tex" | |
| 63026 | 499 | |
| 69422 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 500 | session Typeclass_Hierarchy (doc) in "Typeclass_Hierarchy" = HOL + | 
| 63026 | 501 | options [document_variants = "typeclass_hierarchy"] | 
| 69422 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 502 | sessions | 
| 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 503 | "HOL-Library" | 
| 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 504 | theories [document = false] | 
| 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 505 | Setup | 
| 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 506 | theories | 
| 
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
 wenzelm parents: 
69105diff
changeset | 507 | Typeclass_Hierarchy | 
| 63026 | 508 | document_files (in "..") | 
| 509 | "prepare_document" | |
| 510 | "pdfsetup.sty" | |
| 511 | "iman.sty" | |
| 512 | "extra.sty" | |
| 513 | "isar.sty" | |
| 514 | "manual.bib" | |
| 515 | document_files | |
| 516 | "build" | |
| 517 | "root.tex" | |
| 518 | "style.sty" |