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