| author | wenzelm | 
| Sun, 30 Aug 2015 21:26:42 +0200 | |
| changeset 61057 | 5f6a1e31f3ad | 
| parent 60674 | 2f66099fb472 | 
| child 62013 | 92a2372a226b | 
| 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 | |
| 59378 
065f349852e6
separate image for prerequisites of codegen tutorial
 haftmann parents: 
59175diff
changeset | 19 | session Codegen_Basics in "Codegen" = "HOL" + | 
| 59405 | 20 | options [document = false] | 
| 21 | theories | |
| 59378 
065f349852e6
separate image for prerequisites of codegen tutorial
 haftmann parents: 
59175diff
changeset | 22 | Setup | 
| 
065f349852e6
separate image for prerequisites of codegen tutorial
 haftmann parents: 
59175diff
changeset | 23 | |
| 
065f349852e6
separate image for prerequisites of codegen tutorial
 haftmann parents: 
59175diff
changeset | 24 | session Codegen (doc) in "Codegen" = "Codegen_Basics" + | 
| 48951 
b9238cbcdd41
more standard document preparation within session context;
 wenzelm parents: 
48950diff
changeset | 25 | options [document_variants = "codegen", print_mode = "no_brackets,iff"] | 
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 26 | theories | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 27 | Introduction | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 28 | Foundations | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 29 | Refinement | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 30 | Inductive_Predicate | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 31 | Evaluation | 
| 
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 | |
| 55073 | 46 | session Datatypes (doc) in "Datatypes" = HOL + | 
| 53618 | 47 | options [document_variants = "datatypes"] | 
| 52822 | 48 | theories [document = false] Setup | 
| 52792 
3e651be14fcd
sketched documentation for new (co)datatype package
 blanchet parents: 
52742diff
changeset | 49 | theories Datatypes | 
| 56534 | 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" | |
| 52792 
3e651be14fcd
sketched documentation for new (co)datatype package
 blanchet parents: 
52742diff
changeset | 61 | |
| 60288 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 62 | session Eisbach (doc) in "Eisbach" = "HOL-Eisbach" + | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 63 | options [document_variants = "eisbach", quick_and_dirty, | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 64 | print_mode = "no_brackets,iff", show_question_marks = false] | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 65 | theories [document = false] | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 66 | Base | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 67 | theories | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 68 | Preface | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 69 | Manual | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 70 | document_files (in "..") | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 71 | "prepare_document" | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 72 | "pdfsetup.sty" | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 73 | "iman.sty" | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 74 | "extra.sty" | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 75 | "isar.sty" | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 76 | "ttbox.sty" | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 77 | "underscore.sty" | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 78 | "manual.bib" | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 79 | document_files | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 80 | "build" | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 81 | "root.tex" | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 82 | "style.sty" | 
| 
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
 wenzelm parents: 
60255diff
changeset | 83 | |
| 48948 
fa49f8890ef3
more standard document preparation within session context;
 wenzelm parents: 
48947diff
changeset | 84 | session Functions (doc) in "Functions" = HOL + | 
| 54017 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
 krauss parents: 
53769diff
changeset | 85 | 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 | 86 | theories Functions | 
| 56534 | 87 | document_files (in "..") | 
| 88 | "prepare_document" | |
| 89 | "pdfsetup.sty" | |
| 90 | "iman.sty" | |
| 91 | "extra.sty" | |
| 92 | "isar.sty" | |
| 93 | "manual.bib" | |
| 94 | document_files | |
| 95 | "build" | |
| 96 | "conclusion.tex" | |
| 97 | "intro.tex" | |
| 98 | "mathpartir.sty" | |
| 99 | "root.tex" | |
| 100 | "style.sty" | |
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 101 | |
| 57393 
84e8d378eb5e
suppress documentation "how_to_prove_it" for now, notably for release;
 wenzelm parents: 
57339diff
changeset | 102 | session How_to_Prove_it (* FIXME (doc) *) in "How_to_Prove_it" = HOL + | 
| 56825 | 103 | options [document_variants = "how_to_prove_it", show_question_marks = false] | 
| 104 | theories | |
| 105 | How_to_Prove_it | |
| 106 | document_files | |
| 107 | "root.tex" | |
| 108 | "root.bib" | |
| 109 | "prelude.tex" | |
| 110 | ||
| 48969 | 111 | session Intro (doc) in "Intro" = Pure + | 
| 112 | options [document_variants = "intro"] | |
| 113 | theories | |
| 56534 | 114 | document_files (in "..") | 
| 115 | "prepare_document" | |
| 116 | "pdfsetup.sty" | |
| 117 | "iman.sty" | |
| 118 | "extra.sty" | |
| 119 | "ttbox.sty" | |
| 120 | "manual.bib" | |
| 121 | document_files | |
| 122 | "advanced.tex" | |
| 123 | "build" | |
| 124 | "foundations.tex" | |
| 125 | "getting.tex" | |
| 126 | "root.tex" | |
| 48969 | 127 | |
| 56420 
b266e7a86485
closer correspondence of document and session names, while maintaining document names for external reference
 haftmann parents: 
55385diff
changeset | 128 | session Implementation (doc) in "Implementation" = "HOL-Proofs" + | 
| 58801 | 129 | options [document_variants = "implementation", quick_and_dirty] | 
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 130 | theories | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 131 | Eq | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 132 | Integration | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 133 | Isar | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 134 | Local_Theory | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 135 | ML | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 136 | Prelim | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 137 | Proof | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 138 | Syntax | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 139 | Tactic | 
| 52499 | 140 | theories [parallel_proofs = 0] | 
| 52410 | 141 | Logic | 
| 56534 | 142 | document_files (in "..") | 
| 143 | "prepare_document" | |
| 144 | "pdfsetup.sty" | |
| 145 | "iman.sty" | |
| 146 | "extra.sty" | |
| 147 | "isar.sty" | |
| 148 | "ttbox.sty" | |
| 149 | "underscore.sty" | |
| 150 | "manual.bib" | |
| 151 | document_files | |
| 152 | "build" | |
| 153 | "root.tex" | |
| 154 | "style.sty" | |
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 155 | |
| 56451 
856492b0f755
even more standardized doc session names after #b266e7a86485
 haftmann parents: 
56420diff
changeset | 156 | session Isar_Ref (doc) in "Isar_Ref" = HOL + | 
| 48958 
12afbf6eb7f9
more standard document preparation within session context;
 wenzelm parents: 
48957diff
changeset | 157 | options [document_variants = "isar-ref", quick_and_dirty, thy_output_source] | 
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 158 | theories | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 159 | Preface | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 160 | Synopsis | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 161 | Framework | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 162 | First_Order_Logic | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 163 | Outer_Syntax | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 164 | Document_Preparation | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 165 | Spec | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 166 | Proof | 
| 60484 | 167 | Proof_Script | 
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 168 | Inner_Syntax | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 169 | Generic | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 170 | HOL_Specific | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 171 | Quick_Reference | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 172 | Symbols | 
| 56534 | 173 | document_files (in "..") | 
| 174 | "prepare_document" | |
| 175 | "pdfsetup.sty" | |
| 176 | "iman.sty" | |
| 177 | "extra.sty" | |
| 178 | "isar.sty" | |
| 179 | "ttbox.sty" | |
| 180 | "underscore.sty" | |
| 181 | "manual.bib" | |
| 182 | document_files | |
| 183 | "build" | |
| 184 | "isar-vm.pdf" | |
| 185 | "isar-vm.svg" | |
| 186 | "root.tex" | |
| 187 | "showsymbols" | |
| 188 | "style.sty" | |
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 189 | |
| 54354 | 190 | session JEdit (doc) in "JEdit" = HOL + | 
| 53769 | 191 | options [document_variants = "jedit", thy_output_source] | 
| 192 | theories | |
| 193 | JEdit | |
| 56534 | 194 | document_files (in "..") | 
| 195 | "extra.sty" | |
| 196 | "iman.sty" | |
| 197 | "isar.sty" | |
| 198 | "manual.bib" | |
| 199 | "pdfsetup.sty" | |
| 200 | "prepare_document" | |
| 201 | "ttbox.sty" | |
| 202 | "underscore.sty" | |
| 203 | document_files (in "../Isar_Ref/document") | |
| 204 | "style.sty" | |
| 205 | document_files | |
| 206 | "auto-tools.png" | |
| 60255 
0466bd194d74
more on Isabelle document preparation and bibtex files;
 wenzelm parents: 
59405diff
changeset | 207 | "bibtex-mode.png" | 
| 56534 | 208 | "build" | 
| 60255 
0466bd194d74
more on Isabelle document preparation and bibtex files;
 wenzelm parents: 
59405diff
changeset | 209 | "cite-completion.png" | 
| 56534 | 210 | "isabelle-jedit.png" | 
| 60291 | 211 | "isabelle-jedit-hdpi.png" | 
| 56534 | 212 | "output.png" | 
| 57312 | 213 | "query.png" | 
| 56534 | 214 | "popup1.png" | 
| 215 | "popup2.png" | |
| 216 | "root.tex" | |
| 57336 | 217 | "sidekick.png" | 
| 60255 
0466bd194d74
more on Isabelle document preparation and bibtex files;
 wenzelm parents: 
59405diff
changeset | 218 | "sidekick-document.png" | 
| 56534 | 219 | "sledgehammer.png" | 
| 57339 | 220 | "theories.png" | 
| 53769 | 221 | |
| 56420 
b266e7a86485
closer correspondence of document and session names, while maintaining document names for external reference
 haftmann parents: 
55385diff
changeset | 222 | session Sugar (doc) in "Sugar" = HOL + | 
| 48949 
a773af3e37d6
more standard document preparation within session context;
 wenzelm parents: 
48948diff
changeset | 223 | options [document_variants = "sugar"] | 
| 
a773af3e37d6
more standard document preparation within session context;
 wenzelm parents: 
48948diff
changeset | 224 | theories [document = ""] | 
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 225 | "~~/src/HOL/Library/LaTeXsugar" | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 226 | "~~/src/HOL/Library/OptionalSugar" | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 227 | theories Sugar | 
| 56534 | 228 | document_files (in "..") | 
| 229 | "prepare_document" | |
| 230 | "pdfsetup.sty" | |
| 231 | document_files | |
| 232 | "build" | |
| 233 | "mathpartir.sty" | |
| 234 | "root.bib" | |
| 235 | "root.tex" | |
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 236 | |
| 48943 
54da920baf38
more standard document preparation within session context;
 wenzelm parents: 
48942diff
changeset | 237 | session Locales (doc) in "Locales" = HOL + | 
| 59175 
bf465f335e85
system option "pretty_margin" is superseded by "thy_output_margin";
 wenzelm parents: 
58801diff
changeset | 238 | 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 | 239 | theories | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 240 | Examples1 | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 241 | Examples2 | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 242 | Examples3 | 
| 56534 | 243 | document_files (in "..") | 
| 244 | "prepare_document" | |
| 245 | "pdfsetup.sty" | |
| 246 | document_files | |
| 247 | "build" | |
| 248 | "root.bib" | |
| 249 | "root.tex" | |
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 250 | |
| 48942 
75d8778f94d3
more standard document preparation within session context;
 wenzelm parents: 
48941diff
changeset | 251 | session Logics (doc) in "Logics" = Pure + | 
| 
75d8778f94d3
more standard document preparation within session context;
 wenzelm parents: 
48941diff
changeset | 252 | options [document_variants = "logics"] | 
| 
75d8778f94d3
more standard document preparation within session context;
 wenzelm parents: 
48941diff
changeset | 253 | theories | 
| 56534 | 254 | document_files (in "..") | 
| 255 | "prepare_document" | |
| 256 | "pdfsetup.sty" | |
| 257 | "iman.sty" | |
| 258 | "extra.sty" | |
| 259 | "ttbox.sty" | |
| 260 | "manual.bib" | |
| 261 | document_files | |
| 262 | "CTT.tex" | |
| 263 | "HOL.tex" | |
| 264 | "LK.tex" | |
| 265 | "Sequents.tex" | |
| 266 | "build" | |
| 267 | "preface.tex" | |
| 268 | "root.tex" | |
| 269 | "syntax.tex" | |
| 48945 
b5758f5a469c
more standard document preparation within session context;
 wenzelm parents: 
48944diff
changeset | 270 | |
| 56451 
856492b0f755
even more standardized doc session names after #b266e7a86485
 haftmann parents: 
56420diff
changeset | 271 | session Logics_ZF (doc) in "Logics_ZF" = ZF + | 
| 48956 | 272 | options [document_variants = "logics-ZF", print_mode = "brackets", | 
| 273 | thy_output_source] | |
| 48946 
a9b8344f5196
more standard document preparation within session context;
 wenzelm parents: 
48945diff
changeset | 274 | theories | 
| 
a9b8344f5196
more standard document preparation within session context;
 wenzelm parents: 
48945diff
changeset | 275 | IFOL_examples | 
| 
a9b8344f5196
more standard document preparation within session context;
 wenzelm parents: 
48945diff
changeset | 276 | FOL_examples | 
| 
a9b8344f5196
more standard document preparation within session context;
 wenzelm parents: 
48945diff
changeset | 277 | ZF_examples | 
| 
a9b8344f5196
more standard document preparation within session context;
 wenzelm parents: 
48945diff
changeset | 278 | If | 
| 48956 | 279 | ZF_Isar | 
| 56534 | 280 | document_files (in "..") | 
| 281 | "prepare_document" | |
| 282 | "pdfsetup.sty" | |
| 283 | "isar.sty" | |
| 284 | "ttbox.sty" | |
| 285 | "manual.bib" | |
| 286 | document_files (in "../Logics/document") | |
| 287 | "syntax.tex" | |
| 288 | document_files | |
| 289 | "FOL.tex" | |
| 290 | "ZF.tex" | |
| 291 | "build" | |
| 292 | "logics.sty" | |
| 293 | "root.tex" | |
| 48946 
a9b8344f5196
more standard document preparation within session context;
 wenzelm parents: 
48945diff
changeset | 294 | |
| 48944 
ac15a85e9282
more standard document preparation within session context;
 wenzelm parents: 
48943diff
changeset | 295 | session Main (doc) in "Main" = HOL + | 
| 
ac15a85e9282
more standard document preparation within session context;
 wenzelm parents: 
48943diff
changeset | 296 | options [document_variants = "main"] | 
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 297 | theories Main_Doc | 
| 56534 | 298 | document_files (in "..") | 
| 299 | "prepare_document" | |
| 300 | "pdfsetup.sty" | |
| 301 | document_files | |
| 302 | "build" | |
| 303 | "root.tex" | |
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 304 | |
| 48963 
f11d88bfa934
more standard document preparation within session context;
 wenzelm parents: 
48962diff
changeset | 305 | session Nitpick (doc) in "Nitpick" = Pure + | 
| 
f11d88bfa934
more standard document preparation within session context;
 wenzelm parents: 
48962diff
changeset | 306 | options [document_variants = "nitpick"] | 
| 
f11d88bfa934
more standard document preparation within session context;
 wenzelm parents: 
48962diff
changeset | 307 | theories | 
| 56534 | 308 | document_files (in "..") | 
| 309 | "prepare_document" | |
| 310 | "pdfsetup.sty" | |
| 311 | "iman.sty" | |
| 312 | "manual.bib" | |
| 313 | document_files | |
| 314 | "build" | |
| 315 | "root.tex" | |
| 48963 
f11d88bfa934
more standard document preparation within session context;
 wenzelm parents: 
48962diff
changeset | 316 | |
| 56451 
856492b0f755
even more standardized doc session names after #b266e7a86485
 haftmann parents: 
56420diff
changeset | 317 | session Prog_Prove (doc) in "Prog_Prove" = HOL + | 
| 48947 
7eee8b2d2099
more standard document preparation within session context;
 wenzelm parents: 
48946diff
changeset | 318 | options [document_variants = "prog-prove", show_question_marks = false] | 
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 319 | theories | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 320 | Basics | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 321 | Bool_nat_list | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 322 | MyList | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 323 | Types_and_funs | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 324 | Logic | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 325 | Isar | 
| 56534 | 326 | document_files (in ".") | 
| 327 | "MyList.thy" | |
| 328 | document_files (in "..") | |
| 329 | "prepare_document" | |
| 330 | "pdfsetup.sty" | |
| 331 | document_files | |
| 332 | "bang.pdf" | |
| 333 | "build" | |
| 334 | "intro-isabelle.tex" | |
| 335 | "mathpartir.sty" | |
| 336 | "prelude.tex" | |
| 337 | "root.bib" | |
| 338 | "root.tex" | |
| 339 | "svmono.cls" | |
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 340 | |
| 48962 
a1acc1cb0271
more standard document preparation within session context;
 wenzelm parents: 
48961diff
changeset | 341 | session Sledgehammer (doc) in "Sledgehammer" = Pure + | 
| 
a1acc1cb0271
more standard document preparation within session context;
 wenzelm parents: 
48961diff
changeset | 342 | options [document_variants = "sledgehammer"] | 
| 
a1acc1cb0271
more standard document preparation within session context;
 wenzelm parents: 
48961diff
changeset | 343 | theories | 
| 56534 | 344 | document_files (in "..") | 
| 345 | "prepare_document" | |
| 346 | "pdfsetup.sty" | |
| 347 | "iman.sty" | |
| 348 | "manual.bib" | |
| 349 | document_files | |
| 350 | "build" | |
| 351 | "root.tex" | |
| 48962 
a1acc1cb0271
more standard document preparation within session context;
 wenzelm parents: 
48961diff
changeset | 352 | |
| 48937 
e7418f8d49fe
more standard document preparation within session context;
 wenzelm parents: 
48738diff
changeset | 353 | session System (doc) in "System" = Pure + | 
| 
e7418f8d49fe
more standard document preparation within session context;
 wenzelm parents: 
48738diff
changeset | 354 | options [document_variants = "system", thy_output_source] | 
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 355 | theories | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 356 | Basics | 
| 48578 | 357 | Sessions | 
| 358 | Presentation | |
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 359 | Scala | 
| 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 360 | Misc | 
| 56534 | 361 | document_files (in "..") | 
| 362 | "prepare_document" | |
| 363 | "pdfsetup.sty" | |
| 364 | "iman.sty" | |
| 365 | "extra.sty" | |
| 366 | "isar.sty" | |
| 367 | "ttbox.sty" | |
| 368 | "underscore.sty" | |
| 369 | "manual.bib" | |
| 370 | document_files (in "../Isar_Ref/document") | |
| 371 | "style.sty" | |
| 372 | document_files | |
| 373 | "browser_screenshot.png" | |
| 374 | "build" | |
| 375 | "root.tex" | |
| 48502 
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
 wenzelm parents: diff
changeset | 376 | |
| 48985 | 377 | session Tutorial (doc) in "Tutorial" = HOL + | 
| 51558 
91f8bed6d0a4
allow build with skip_proofs enabled -- disable it for sessions that would fail due to embedded diagnostic commands, for example;
 wenzelm parents: 
51397diff
changeset | 378 | options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false] | 
| 53376 | 379 | theories [threads = 1] | 
| 380 | "ToyList/ToyList_Test" | |
| 48526 | 381 | theories [thy_output_indent = 5] | 
| 382 | "ToyList/ToyList" | |
| 383 | "Ifexpr/Ifexpr" | |
| 384 | "CodeGen/CodeGen" | |
| 385 | "Trie/Trie" | |
| 386 | "Datatype/ABexpr" | |
| 387 | "Datatype/unfoldnested" | |
| 388 | "Datatype/Nested" | |
| 389 | "Datatype/Fundata" | |
| 390 | "Fun/fun0" | |
| 391 | "Advanced/simp2" | |
| 392 | "CTL/PDL" | |
| 393 | "CTL/CTL" | |
| 394 | "CTL/CTLind" | |
| 395 | "Inductive/Even" | |
| 396 | "Inductive/Mutual" | |
| 397 | "Inductive/Star" | |
| 398 | "Inductive/AB" | |
| 399 | "Inductive/Advanced" | |
| 400 | "Misc/Tree" | |
| 401 | "Misc/Tree2" | |
| 402 | "Misc/Plus" | |
| 403 | "Misc/case_exprs" | |
| 404 | "Misc/fakenat" | |
| 405 | "Misc/natsum" | |
| 406 | "Misc/pairs2" | |
| 407 | "Misc/Option2" | |
| 408 | "Misc/types" | |
| 409 | "Misc/prime_def" | |
| 410 | "Misc/simp" | |
| 411 | "Misc/Itrev" | |
| 412 | "Misc/AdvancedInd" | |
| 413 | "Misc/appendix" | |
| 414 | theories | |
| 415 | "Protocol/NS_Public" | |
| 416 | "Documents/Documents" | |
| 48966 
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
 wenzelm parents: 
48963diff
changeset | 417 | theories [document = ""] | 
| 48526 | 418 | "Types/Setup" | 
| 59175 
bf465f335e85
system option "pretty_margin" is superseded by "thy_output_margin";
 wenzelm parents: 
58801diff
changeset | 419 | theories [thy_output_margin = 64, thy_output_indent = 0] | 
| 48526 | 420 | "Types/Numbers" | 
| 421 | "Types/Pairs" | |
| 422 | "Types/Records" | |
| 423 | "Types/Typedefs" | |
| 424 | "Types/Overloading" | |
| 425 | "Types/Axioms" | |
| 426 | "Rules/Basic" | |
| 427 | "Rules/Blast" | |
| 428 | "Rules/Force" | |
| 59175 
bf465f335e85
system option "pretty_margin" is superseded by "thy_output_margin";
 wenzelm parents: 
58801diff
changeset | 429 | 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 | 430 | "Rules/TPrimes" | 
| 48526 | 431 | "Rules/Forward" | 
| 432 | "Rules/Tacticals" | |
| 433 | "Rules/find2" | |
| 434 | "Sets/Examples" | |
| 435 | "Sets/Functions" | |
| 436 | "Sets/Relations" | |
| 437 | "Sets/Recur" | |
| 56534 | 438 | document_files (in "ToyList") | 
| 57083 | 439 | "ToyList1.txt" | 
| 440 | "ToyList2.txt" | |
| 56534 | 441 | document_files (in "..") | 
| 442 | "pdfsetup.sty" | |
| 443 | "ttbox.sty" | |
| 444 | "manual.bib" | |
| 445 | document_files | |
| 446 | "advanced0.tex" | |
| 447 | "appendix0.tex" | |
| 448 | "basics.tex" | |
| 449 | "build" | |
| 450 | "cl2emono-modified.sty" | |
| 451 | "ctl0.tex" | |
| 452 | "documents0.tex" | |
| 453 | "fp.tex" | |
| 454 | "inductive0.tex" | |
| 455 | "isa-index" | |
| 456 | "Isa-logics.pdf" | |
| 457 | "numerics.tex" | |
| 458 | "pghead.pdf" | |
| 459 | "preface.tex" | |
| 460 | "protocol.tex" | |
| 461 | "root.tex" | |
| 462 | "rules.tex" | |
| 463 | "sets.tex" | |
| 464 | "tutorial.sty" | |
| 465 | "typedef.pdf" | |
| 466 | "types0.tex" |