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