wenzelm@49965
|
1 |
session Classes (doc) in "Classes" = HOL +
|
wenzelm@49965
|
2 |
options [document_variants = "classes"]
|
wenzelm@49517
|
3 |
theories [document = false] Setup
|
wenzelm@49517
|
4 |
theories Classes
|
wenzelm@49965
|
5 |
files
|
wenzelm@49986
|
6 |
"../prepare_document"
|
wenzelm@49971
|
7 |
"../pdfsetup.sty"
|
wenzelm@50333
|
8 |
"../iman.sty"
|
wenzelm@50333
|
9 |
"../extra.sty"
|
wenzelm@50333
|
10 |
"../isar.sty"
|
wenzelm@50333
|
11 |
"../manual.bib"
|
wenzelm@49965
|
12 |
"document/build"
|
wenzelm@49965
|
13 |
"document/root.tex"
|
wenzelm@49965
|
14 |
"document/style.sty"
|
wenzelm@49517
|
15 |
|
wenzelm@49966
|
16 |
session Codegen (doc) in "Codegen" = "HOL-Library" +
|
wenzelm@49966
|
17 |
options [document_variants = "codegen", print_mode = "no_brackets,iff"]
|
wenzelm@49517
|
18 |
theories [document = false] Setup
|
wenzelm@49517
|
19 |
theories
|
wenzelm@49517
|
20 |
Introduction
|
wenzelm@49517
|
21 |
Foundations
|
wenzelm@49517
|
22 |
Refinement
|
wenzelm@49517
|
23 |
Inductive_Predicate
|
wenzelm@49517
|
24 |
Evaluation
|
wenzelm@49517
|
25 |
Adaptation
|
wenzelm@49517
|
26 |
Further
|
wenzelm@49966
|
27 |
files
|
wenzelm@49986
|
28 |
"../prepare_document"
|
wenzelm@49971
|
29 |
"../pdfsetup.sty"
|
wenzelm@50333
|
30 |
"../iman.sty"
|
wenzelm@50333
|
31 |
"../extra.sty"
|
wenzelm@50333
|
32 |
"../isar.sty"
|
wenzelm@50333
|
33 |
"../manual.bib"
|
wenzelm@49969
|
34 |
"document/adapt.tex"
|
wenzelm@49966
|
35 |
"document/architecture.tex"
|
wenzelm@49966
|
36 |
"document/build"
|
wenzelm@49966
|
37 |
"document/root.tex"
|
wenzelm@49966
|
38 |
"document/style.sty"
|
wenzelm@49517
|
39 |
|
wenzelm@49963
|
40 |
session Functions (doc) in "Functions" = HOL +
|
wenzelm@49963
|
41 |
options [document_variants = "functions"]
|
wenzelm@49517
|
42 |
theories Functions
|
wenzelm@49963
|
43 |
files
|
wenzelm@49986
|
44 |
"../prepare_document"
|
wenzelm@49971
|
45 |
"../pdfsetup.sty"
|
wenzelm@49963
|
46 |
"../iman.sty"
|
wenzelm@49963
|
47 |
"../extra.sty"
|
wenzelm@49963
|
48 |
"../isar.sty"
|
wenzelm@49963
|
49 |
"../manual.bib"
|
wenzelm@49963
|
50 |
"document/build"
|
wenzelm@49963
|
51 |
"document/conclusion.tex"
|
wenzelm@49963
|
52 |
"document/intro.tex"
|
wenzelm@49963
|
53 |
"document/mathpartir.sty"
|
wenzelm@49963
|
54 |
"document/root.tex"
|
wenzelm@49963
|
55 |
"document/style.sty"
|
wenzelm@49517
|
56 |
|
wenzelm@49984
|
57 |
session Intro (doc) in "Intro" = Pure +
|
wenzelm@49984
|
58 |
options [document_variants = "intro"]
|
wenzelm@49984
|
59 |
theories
|
wenzelm@49984
|
60 |
files
|
wenzelm@49986
|
61 |
"../prepare_document"
|
wenzelm@49984
|
62 |
"../pdfsetup.sty"
|
wenzelm@49984
|
63 |
"../iman.sty"
|
wenzelm@49984
|
64 |
"../extra.sty"
|
wenzelm@49984
|
65 |
"../ttbox.sty"
|
wenzelm@49984
|
66 |
"../manual.bib"
|
wenzelm@49984
|
67 |
"document/build"
|
wenzelm@49984
|
68 |
"document/root.tex"
|
wenzelm@49984
|
69 |
|
wenzelm@49953
|
70 |
session IsarImplementation (doc) in "IsarImplementation" = HOL +
|
wenzelm@49953
|
71 |
options [document_variants = "implementation"]
|
wenzelm@49517
|
72 |
theories
|
wenzelm@49517
|
73 |
Eq
|
wenzelm@49517
|
74 |
Integration
|
wenzelm@49517
|
75 |
Isar
|
wenzelm@49517
|
76 |
Local_Theory
|
wenzelm@49517
|
77 |
Logic
|
wenzelm@49517
|
78 |
ML
|
wenzelm@49517
|
79 |
Prelim
|
wenzelm@49517
|
80 |
Proof
|
wenzelm@49517
|
81 |
Syntax
|
wenzelm@49517
|
82 |
Tactic
|
wenzelm@49953
|
83 |
files
|
wenzelm@49986
|
84 |
"../prepare_document"
|
wenzelm@49971
|
85 |
"../pdfsetup.sty"
|
wenzelm@49953
|
86 |
"../iman.sty"
|
wenzelm@49953
|
87 |
"../extra.sty"
|
wenzelm@49953
|
88 |
"../isar.sty"
|
wenzelm@50333
|
89 |
"../ttbox.sty"
|
wenzelm@49953
|
90 |
"../underscore.sty"
|
wenzelm@49953
|
91 |
"../manual.bib"
|
wenzelm@49953
|
92 |
"document/build"
|
wenzelm@49953
|
93 |
"document/root.tex"
|
wenzelm@49953
|
94 |
"document/style.sty"
|
wenzelm@49517
|
95 |
|
wenzelm@49973
|
96 |
session IsarRef (doc) in "IsarRef" = HOL +
|
wenzelm@49973
|
97 |
options [document_variants = "isar-ref", quick_and_dirty, thy_output_source]
|
wenzelm@49517
|
98 |
theories
|
wenzelm@49517
|
99 |
Preface
|
wenzelm@49517
|
100 |
Synopsis
|
wenzelm@49517
|
101 |
Framework
|
wenzelm@49517
|
102 |
First_Order_Logic
|
wenzelm@49517
|
103 |
Outer_Syntax
|
wenzelm@49517
|
104 |
Document_Preparation
|
wenzelm@49517
|
105 |
Spec
|
wenzelm@49517
|
106 |
Proof
|
wenzelm@49517
|
107 |
Inner_Syntax
|
wenzelm@49517
|
108 |
Misc
|
wenzelm@49517
|
109 |
Generic
|
wenzelm@49517
|
110 |
HOL_Specific
|
wenzelm@49517
|
111 |
Quick_Reference
|
wenzelm@49517
|
112 |
Symbols
|
wenzelm@49517
|
113 |
ML_Tactic
|
wenzelm@49973
|
114 |
files
|
wenzelm@49986
|
115 |
"../prepare_document"
|
wenzelm@49973
|
116 |
"../pdfsetup.sty"
|
wenzelm@49973
|
117 |
"../iman.sty"
|
wenzelm@49973
|
118 |
"../extra.sty"
|
wenzelm@50333
|
119 |
"../isar.sty"
|
wenzelm@49973
|
120 |
"../ttbox.sty"
|
wenzelm@50333
|
121 |
"../underscore.sty"
|
wenzelm@49973
|
122 |
"../manual.bib"
|
wenzelm@49973
|
123 |
"document/build"
|
wenzelm@49973
|
124 |
"document/isar-vm.eps"
|
wenzelm@49973
|
125 |
"document/isar-vm.pdf"
|
wenzelm@49973
|
126 |
"document/isar-vm.svg"
|
wenzelm@49973
|
127 |
"document/root.tex"
|
wenzelm@49973
|
128 |
"document/showsymbols"
|
wenzelm@49973
|
129 |
"document/style.sty"
|
wenzelm@49517
|
130 |
|
wenzelm@49964
|
131 |
session LaTeXsugar (doc) in "LaTeXsugar" = HOL +
|
wenzelm@49964
|
132 |
options [document_variants = "sugar"]
|
wenzelm@49964
|
133 |
theories [document = ""]
|
wenzelm@49517
|
134 |
"~~/src/HOL/Library/LaTeXsugar"
|
wenzelm@49517
|
135 |
"~~/src/HOL/Library/OptionalSugar"
|
wenzelm@49517
|
136 |
theories Sugar
|
wenzelm@49964
|
137 |
files
|
wenzelm@49986
|
138 |
"../prepare_document"
|
wenzelm@49971
|
139 |
"../pdfsetup.sty"
|
wenzelm@49964
|
140 |
"document/build"
|
wenzelm@49964
|
141 |
"document/mathpartir.sty"
|
wenzelm@49964
|
142 |
"document/root.bib"
|
wenzelm@49964
|
143 |
"document/root.tex"
|
wenzelm@49517
|
144 |
|
wenzelm@49958
|
145 |
session Locales (doc) in "Locales" = HOL +
|
wenzelm@49970
|
146 |
options [document_variants = "locales", pretty_margin = 65]
|
wenzelm@49517
|
147 |
theories
|
wenzelm@49517
|
148 |
Examples1
|
wenzelm@49517
|
149 |
Examples2
|
wenzelm@49517
|
150 |
Examples3
|
wenzelm@49958
|
151 |
files
|
wenzelm@49986
|
152 |
"../prepare_document"
|
wenzelm@49971
|
153 |
"../pdfsetup.sty"
|
wenzelm@49958
|
154 |
"document/build"
|
wenzelm@49958
|
155 |
"document/root.tex"
|
wenzelm@49517
|
156 |
|
wenzelm@49957
|
157 |
session Logics (doc) in "Logics" = Pure +
|
wenzelm@49957
|
158 |
options [document_variants = "logics"]
|
wenzelm@49957
|
159 |
theories
|
wenzelm@49957
|
160 |
files
|
wenzelm@49986
|
161 |
"../prepare_document"
|
wenzelm@49971
|
162 |
"../pdfsetup.sty"
|
wenzelm@49957
|
163 |
"../iman.sty"
|
wenzelm@49957
|
164 |
"../extra.sty"
|
wenzelm@49957
|
165 |
"../ttbox.sty"
|
wenzelm@49957
|
166 |
"../manual.bib"
|
wenzelm@49957
|
167 |
"document/build"
|
wenzelm@49957
|
168 |
"document/root.tex"
|
wenzelm@49957
|
169 |
|
wenzelm@49960
|
170 |
session "Logics-HOL" (doc) in "HOL" = Pure +
|
wenzelm@49960
|
171 |
options [document_variants = "logics-HOL"]
|
wenzelm@49960
|
172 |
theories
|
wenzelm@49960
|
173 |
files
|
wenzelm@49986
|
174 |
"../prepare_document"
|
wenzelm@49971
|
175 |
"../pdfsetup.sty"
|
wenzelm@49960
|
176 |
"../iman.sty"
|
wenzelm@49960
|
177 |
"../extra.sty"
|
wenzelm@49960
|
178 |
"../ttbox.sty"
|
wenzelm@49960
|
179 |
"../manual.bib"
|
wenzelm@49960
|
180 |
"../Logics/document/syntax.tex"
|
wenzelm@49960
|
181 |
"document/build"
|
wenzelm@49960
|
182 |
"document/root.tex"
|
wenzelm@49960
|
183 |
|
wenzelm@49961
|
184 |
session "Logics-ZF" (doc) in "ZF" = ZF +
|
wenzelm@49971
|
185 |
options [document_variants = "logics-ZF", print_mode = "brackets",
|
wenzelm@49971
|
186 |
thy_output_source]
|
wenzelm@49961
|
187 |
theories
|
wenzelm@49961
|
188 |
IFOL_examples
|
wenzelm@49961
|
189 |
FOL_examples
|
wenzelm@49961
|
190 |
ZF_examples
|
wenzelm@49961
|
191 |
If
|
wenzelm@49971
|
192 |
ZF_Isar
|
wenzelm@49961
|
193 |
files
|
wenzelm@49986
|
194 |
"../prepare_document"
|
wenzelm@49971
|
195 |
"../pdfsetup.sty"
|
wenzelm@49971
|
196 |
"../isar.sty"
|
wenzelm@49961
|
197 |
"../ttbox.sty"
|
wenzelm@49961
|
198 |
"../manual.bib"
|
wenzelm@49961
|
199 |
"../Logics/document/syntax.tex"
|
wenzelm@49961
|
200 |
"document/build"
|
wenzelm@49961
|
201 |
"document/root.tex"
|
wenzelm@49961
|
202 |
|
wenzelm@49959
|
203 |
session Main (doc) in "Main" = HOL +
|
wenzelm@49959
|
204 |
options [document_variants = "main"]
|
wenzelm@49517
|
205 |
theories Main_Doc
|
wenzelm@49959
|
206 |
files
|
wenzelm@49986
|
207 |
"../prepare_document"
|
wenzelm@49971
|
208 |
"../pdfsetup.sty"
|
wenzelm@49959
|
209 |
"document/build"
|
wenzelm@49959
|
210 |
"document/root.tex"
|
wenzelm@49517
|
211 |
|
wenzelm@49978
|
212 |
session Nitpick (doc) in "Nitpick" = Pure +
|
wenzelm@49978
|
213 |
options [document_variants = "nitpick"]
|
wenzelm@49978
|
214 |
theories
|
wenzelm@49978
|
215 |
files
|
wenzelm@49986
|
216 |
"../prepare_document"
|
wenzelm@49978
|
217 |
"../pdfsetup.sty"
|
wenzelm@49978
|
218 |
"../iman.sty"
|
wenzelm@49978
|
219 |
"../manual.bib"
|
wenzelm@49978
|
220 |
"document/build"
|
wenzelm@49978
|
221 |
"document/root.tex"
|
wenzelm@49978
|
222 |
|
wenzelm@49962
|
223 |
session ProgProve (doc) in "ProgProve" = HOL +
|
wenzelm@49962
|
224 |
options [document_variants = "prog-prove", show_question_marks = false]
|
wenzelm@49517
|
225 |
theories
|
wenzelm@49517
|
226 |
Basics
|
wenzelm@49517
|
227 |
Bool_nat_list
|
wenzelm@49517
|
228 |
MyList
|
wenzelm@49517
|
229 |
Types_and_funs
|
wenzelm@49517
|
230 |
Logic
|
wenzelm@49517
|
231 |
Isar
|
wenzelm@49962
|
232 |
files
|
wenzelm@49986
|
233 |
"../prepare_document"
|
wenzelm@49971
|
234 |
"../pdfsetup.sty"
|
wenzelm@49962
|
235 |
"document/bang.eps"
|
wenzelm@49962
|
236 |
"document/bang.pdf"
|
wenzelm@49962
|
237 |
"document/build"
|
wenzelm@49962
|
238 |
"document/intro-isabelle.tex"
|
wenzelm@49962
|
239 |
"document/mathpartir.sty"
|
wenzelm@49962
|
240 |
"document/prelude.tex"
|
wenzelm@49962
|
241 |
"document/root.bib"
|
wenzelm@49962
|
242 |
"document/root.tex"
|
wenzelm@49962
|
243 |
"document/svmono.cls"
|
wenzelm@49517
|
244 |
|
wenzelm@49954
|
245 |
session Ref (doc) in "Ref" = Pure +
|
wenzelm@49954
|
246 |
options [document_variants = "ref"]
|
wenzelm@49954
|
247 |
theories
|
wenzelm@49954
|
248 |
files
|
wenzelm@49986
|
249 |
"../prepare_document"
|
wenzelm@49971
|
250 |
"../pdfsetup.sty"
|
wenzelm@49954
|
251 |
"../iman.sty"
|
wenzelm@49954
|
252 |
"../extra.sty"
|
wenzelm@49954
|
253 |
"../ttbox.sty"
|
wenzelm@49954
|
254 |
"../manual.bib"
|
wenzelm@49954
|
255 |
"document/build"
|
wenzelm@49954
|
256 |
"document/root.tex"
|
wenzelm@49954
|
257 |
"document/syntax.tex"
|
wenzelm@49954
|
258 |
"document/thm.tex"
|
wenzelm@49954
|
259 |
|
wenzelm@49977
|
260 |
session Sledgehammer (doc) in "Sledgehammer" = Pure +
|
wenzelm@49977
|
261 |
options [document_variants = "sledgehammer"]
|
wenzelm@49977
|
262 |
theories
|
wenzelm@49977
|
263 |
files
|
wenzelm@49986
|
264 |
"../prepare_document"
|
wenzelm@49977
|
265 |
"../pdfsetup.sty"
|
wenzelm@49977
|
266 |
"../iman.sty"
|
wenzelm@49977
|
267 |
"../manual.bib"
|
wenzelm@49977
|
268 |
"document/build"
|
wenzelm@49977
|
269 |
"document/root.tex"
|
wenzelm@49977
|
270 |
|
wenzelm@49952
|
271 |
session System (doc) in "System" = Pure +
|
wenzelm@49952
|
272 |
options [document_variants = "system", thy_output_source]
|
wenzelm@49517
|
273 |
theories
|
wenzelm@49517
|
274 |
Basics
|
wenzelm@49517
|
275 |
Interfaces
|
wenzelm@49593
|
276 |
Sessions
|
wenzelm@49593
|
277 |
Presentation
|
wenzelm@49517
|
278 |
Scala
|
wenzelm@49517
|
279 |
Misc
|
wenzelm@49952
|
280 |
files
|
wenzelm@49986
|
281 |
"../prepare_document"
|
wenzelm@49976
|
282 |
"../IsarRef/document/style.sty"
|
wenzelm@49971
|
283 |
"../pdfsetup.sty"
|
wenzelm@49952
|
284 |
"../iman.sty"
|
wenzelm@49952
|
285 |
"../extra.sty"
|
wenzelm@50333
|
286 |
"../isar.sty"
|
wenzelm@49952
|
287 |
"../ttbox.sty"
|
wenzelm@49952
|
288 |
"../underscore.sty"
|
wenzelm@49952
|
289 |
"../manual.bib"
|
wenzelm@49952
|
290 |
"document/browser_screenshot.eps"
|
wenzelm@49952
|
291 |
"document/browser_screenshot.png"
|
wenzelm@49952
|
292 |
"document/build"
|
wenzelm@49952
|
293 |
"document/root.tex"
|
wenzelm@49517
|
294 |
|
wenzelm@50000
|
295 |
session Tutorial (doc) in "Tutorial" = HOL +
|
wenzelm@49981
|
296 |
options [document_variants = "tutorial", print_mode = "brackets"]
|
wenzelm@49541
|
297 |
theories [thy_output_indent = 5]
|
wenzelm@49541
|
298 |
"ToyList/ToyList"
|
wenzelm@49541
|
299 |
"Ifexpr/Ifexpr"
|
wenzelm@49541
|
300 |
"CodeGen/CodeGen"
|
wenzelm@49541
|
301 |
"Trie/Trie"
|
wenzelm@49541
|
302 |
"Datatype/ABexpr"
|
wenzelm@49541
|
303 |
"Datatype/unfoldnested"
|
wenzelm@49541
|
304 |
"Datatype/Nested"
|
wenzelm@49541
|
305 |
"Datatype/Fundata"
|
wenzelm@49541
|
306 |
"Fun/fun0"
|
wenzelm@49541
|
307 |
"Advanced/simp2"
|
wenzelm@49541
|
308 |
"CTL/PDL"
|
wenzelm@49541
|
309 |
"CTL/CTL"
|
wenzelm@49541
|
310 |
"CTL/CTLind"
|
wenzelm@49541
|
311 |
"Inductive/Even"
|
wenzelm@49541
|
312 |
"Inductive/Mutual"
|
wenzelm@49541
|
313 |
"Inductive/Star"
|
wenzelm@49541
|
314 |
"Inductive/AB"
|
wenzelm@49541
|
315 |
"Inductive/Advanced"
|
wenzelm@49541
|
316 |
"Misc/Tree"
|
wenzelm@49541
|
317 |
"Misc/Tree2"
|
wenzelm@49541
|
318 |
"Misc/Plus"
|
wenzelm@49541
|
319 |
"Misc/case_exprs"
|
wenzelm@49541
|
320 |
"Misc/fakenat"
|
wenzelm@49541
|
321 |
"Misc/natsum"
|
wenzelm@49541
|
322 |
"Misc/pairs2"
|
wenzelm@49541
|
323 |
"Misc/Option2"
|
wenzelm@49541
|
324 |
"Misc/types"
|
wenzelm@49541
|
325 |
"Misc/prime_def"
|
wenzelm@49541
|
326 |
"Misc/simp"
|
wenzelm@49541
|
327 |
"Misc/Itrev"
|
wenzelm@49541
|
328 |
"Misc/AdvancedInd"
|
wenzelm@49541
|
329 |
"Misc/appendix"
|
wenzelm@49541
|
330 |
theories
|
wenzelm@49541
|
331 |
"Protocol/NS_Public"
|
wenzelm@49541
|
332 |
"Documents/Documents"
|
wenzelm@49981
|
333 |
theories [document = ""]
|
wenzelm@49541
|
334 |
"Types/Setup"
|
wenzelm@49626
|
335 |
theories [pretty_margin = 64, thy_output_indent = 0]
|
wenzelm@49541
|
336 |
"Types/Numbers"
|
wenzelm@49541
|
337 |
"Types/Pairs"
|
wenzelm@49541
|
338 |
"Types/Records"
|
wenzelm@49541
|
339 |
"Types/Typedefs"
|
wenzelm@49541
|
340 |
"Types/Overloading"
|
wenzelm@49541
|
341 |
"Types/Axioms"
|
wenzelm@49541
|
342 |
"Rules/Basic"
|
wenzelm@49541
|
343 |
"Rules/Blast"
|
wenzelm@49541
|
344 |
"Rules/Force"
|
wenzelm@49626
|
345 |
theories [pretty_margin = 64, thy_output_indent = 5]
|
wenzelm@49626
|
346 |
"Rules/Primes"
|
wenzelm@49541
|
347 |
"Rules/Forward"
|
wenzelm@49541
|
348 |
"Rules/Tacticals"
|
wenzelm@49541
|
349 |
"Rules/find2"
|
wenzelm@49541
|
350 |
"Sets/Examples"
|
wenzelm@49541
|
351 |
"Sets/Functions"
|
wenzelm@49541
|
352 |
"Sets/Relations"
|
wenzelm@49541
|
353 |
"Sets/Recur"
|
wenzelm@49981
|
354 |
files
|
wenzelm@49981
|
355 |
"ToyList/ToyList1"
|
wenzelm@49981
|
356 |
"ToyList/ToyList2"
|
wenzelm@49981
|
357 |
"../pdfsetup.sty"
|
wenzelm@49981
|
358 |
"../ttbox.sty"
|
wenzelm@49981
|
359 |
"../manual.bib"
|
wenzelm@49983
|
360 |
"document/advanced0.tex"
|
wenzelm@49983
|
361 |
"document/appendix0.tex"
|
wenzelm@49983
|
362 |
"document/basics.tex"
|
wenzelm@49983
|
363 |
"document/build"
|
wenzelm@49983
|
364 |
"document/cl2emono-modified.sty"
|
wenzelm@49983
|
365 |
"document/ctl0.tex"
|
wenzelm@49983
|
366 |
"document/documents0.tex"
|
wenzelm@49983
|
367 |
"document/fp.tex"
|
wenzelm@49983
|
368 |
"document/inductive0.tex"
|
wenzelm@49983
|
369 |
"document/isa-index"
|
wenzelm@49983
|
370 |
"document/Isa-logics.eps"
|
wenzelm@49983
|
371 |
"document/Isa-logics.pdf"
|
wenzelm@49983
|
372 |
"document/numerics.tex"
|
wenzelm@49981
|
373 |
"document/pghead.eps"
|
wenzelm@49981
|
374 |
"document/pghead.pdf"
|
wenzelm@49983
|
375 |
"document/preface.tex"
|
wenzelm@49983
|
376 |
"document/protocol.tex"
|
wenzelm@49981
|
377 |
"document/root.tex"
|
wenzelm@49983
|
378 |
"document/rules.tex"
|
wenzelm@49983
|
379 |
"document/sets.tex"
|
wenzelm@49983
|
380 |
"document/tutorial.sty"
|
wenzelm@49983
|
381 |
"document/typedef.pdf"
|
wenzelm@49983
|
382 |
"document/typedef.ps"
|
wenzelm@49983
|
383 |
"document/types0.tex"
|
wenzelm@49517
|
384 |
|