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