1chapter Doc
2
3session Classes (doc) in "Classes" = HOL +
4  options [document_variants = "classes", quick_and_dirty]
5  theories [document = false] Setup
6  theories Classes
7  document_files (in "..")
8    "prepare_document"
9    "pdfsetup.sty"
10    "iman.sty"
11    "extra.sty"
12    "isar.sty"
13    "manual.bib"
14  document_files
15    "build"
16    "root.tex"
17    "style.sty"
18
19session Codegen_Basics in "Codegen" = "HOL-Library" +
20  theories
21    Setup
22
23session Codegen (doc) in "Codegen" = "Codegen_Basics" +
24  options [document_variants = "codegen", print_mode = "no_brackets,iff"]
25  theories
26    Introduction
27    Foundations
28    Refinement
29    Inductive_Predicate
30    Evaluation
31    Computations
32    Adaptation
33    Further
34  document_files (in "..")
35    "prepare_document"
36    "pdfsetup.sty"
37    "iman.sty"
38    "extra.sty"
39    "isar.sty"
40    "manual.bib"
41  document_files
42    "build"
43    "root.tex"
44    "style.sty"
45
46session Corec (doc) in "Corec" = "HOL-Library" +
47  options [document_variants = "corec"]
48  sessions
49    Datatypes
50  theories Corec
51  document_files (in "..")
52    "prepare_document"
53    "pdfsetup.sty"
54    "iman.sty"
55    "extra.sty"
56    "isar.sty"
57    "manual.bib"
58  document_files
59    "build"
60    "root.tex"
61    "style.sty"
62
63session Datatypes (doc) in "Datatypes" = "HOL-Library" +
64  options [document_variants = "datatypes"]
65  theories [document = false] Setup
66  theories Datatypes
67  document_files (in "..")
68    "prepare_document"
69    "pdfsetup.sty"
70    "iman.sty"
71    "extra.sty"
72    "isar.sty"
73    "manual.bib"
74  document_files
75    "build"
76    "root.tex"
77    "style.sty"
78
79session Eisbach (doc) in "Eisbach" = "HOL-Eisbach" +
80  options [document_variants = "eisbach", quick_and_dirty,
81    print_mode = "no_brackets,iff", show_question_marks = false]
82  theories [document = false]
83    Base
84  theories
85    Preface
86    Manual
87  document_files (in "..")
88    "prepare_document"
89    "pdfsetup.sty"
90    "iman.sty"
91    "extra.sty"
92    "isar.sty"
93    "ttbox.sty"
94    "underscore.sty"
95    "manual.bib"
96  document_files
97    "build"
98    "root.tex"
99    "style.sty"
100
101session Functions (doc) in "Functions" = HOL +
102  options [document_variants = "functions", skip_proofs = false, quick_and_dirty]
103  theories Functions
104  document_files (in "..")
105    "prepare_document"
106    "pdfsetup.sty"
107    "iman.sty"
108    "extra.sty"
109    "isar.sty"
110    "manual.bib"
111  document_files
112    "build"
113    "conclusion.tex"
114    "intro.tex"
115    "mathpartir.sty"
116    "root.tex"
117    "style.sty"
118
119session How_to_Prove_it (* FIXME (doc) *) in "How_to_Prove_it" = HOL +
120  options [document_variants = "how_to_prove_it", show_question_marks = false]
121  theories
122    How_to_Prove_it
123  document_files
124    "root.tex"
125    "root.bib"
126    "prelude.tex"
127
128session Intro (doc) in "Intro" = Pure +
129  options [document_variants = "intro"]
130  document_files (in "..")
131    "prepare_document"
132    "pdfsetup.sty"
133    "iman.sty"
134    "extra.sty"
135    "ttbox.sty"
136    "manual.bib"
137  document_files
138    "advanced.tex"
139    "build"
140    "foundations.tex"
141    "getting.tex"
142    "root.tex"
143
144session Implementation (doc) in "Implementation" = "HOL" +
145  options [document_variants = "implementation", quick_and_dirty]
146  theories
147    Eq
148    Integration
149    Isar
150    Local_Theory
151    "ML"
152    Prelim
153    Proof
154    Syntax
155    Tactic
156  theories [parallel_proofs = 0]
157    Logic
158  document_files (in "..")
159    "prepare_document"
160    "pdfsetup.sty"
161    "iman.sty"
162    "extra.sty"
163    "isar.sty"
164    "ttbox.sty"
165    "underscore.sty"
166    "manual.bib"
167  document_files
168    "build"
169    "root.tex"
170    "style.sty"
171
172session Isar_Ref (doc) in "Isar_Ref" = "HOL-Library" +
173  options [document_variants = "isar-ref", quick_and_dirty, thy_output_source]
174  theories
175    Preface
176    Synopsis
177    Framework
178    First_Order_Logic
179    Outer_Syntax
180    Document_Preparation
181    Spec
182    Proof
183    Proof_Script
184    Inner_Syntax
185    Generic
186    HOL_Specific
187    Quick_Reference
188    Symbols
189  document_files (in "..")
190    "prepare_document"
191    "pdfsetup.sty"
192    "iman.sty"
193    "extra.sty"
194    "isar.sty"
195    "ttbox.sty"
196    "underscore.sty"
197    "manual.bib"
198  document_files
199    "build"
200    "isar-vm.pdf"
201    "isar-vm.svg"
202    "root.tex"
203    "showsymbols"
204    "style.sty"
205
206session JEdit (doc) in "JEdit" = HOL +
207  options [document_variants = "jedit", thy_output_source]
208  theories
209    JEdit
210  document_files (in "..")
211    "extra.sty"
212    "iman.sty"
213    "isar.sty"
214    "manual.bib"
215    "pdfsetup.sty"
216    "prepare_document"
217    "ttbox.sty"
218    "underscore.sty"
219  document_files (in "../Isar_Ref/document")
220    "style.sty"
221  document_files
222    "auto-tools.png"
223    "bibtex-mode.png"
224    "build"
225    "cite-completion.png"
226    "isabelle-jedit-hdpi.png"
227    "isabelle-jedit.png"
228    "markdown-document.png"
229    "ml-debugger.png"
230    "output-and-state.png"
231    "output-including-state.png"
232    "output.png"
233    "popup1.png"
234    "popup2.png"
235    "query.png"
236    "root.tex"
237    "scope1.png"
238    "scope2.png"
239    "sidekick-document.png"
240    "sidekick.png"
241    "sledgehammer.png"
242    "theories.png"
243
244session Sugar (doc) in "Sugar" = HOL +
245  options [document_variants = "sugar"]
246  sessions
247    "HOL-Library"
248  theories Sugar
249  document_files (in "..")
250    "prepare_document"
251    "pdfsetup.sty"
252  document_files
253    "build"
254    "mathpartir.sty"
255    "root.bib"
256    "root.tex"
257
258session Locales (doc) in "Locales" = HOL +
259  options [document_variants = "locales", thy_output_margin = 65, skip_proofs = false]
260  theories
261    Examples1
262    Examples2
263    Examples3
264  document_files (in "..")
265    "prepare_document"
266    "pdfsetup.sty"
267  document_files
268    "build"
269    "root.bib"
270    "root.tex"
271
272session Logics (doc) in "Logics" = Pure +
273  options [document_variants = "logics"]
274  document_files (in "..")
275    "prepare_document"
276    "pdfsetup.sty"
277    "iman.sty"
278    "extra.sty"
279    "ttbox.sty"
280    "manual.bib"
281  document_files
282    "CTT.tex"
283    "HOL.tex"
284    "LK.tex"
285    "Sequents.tex"
286    "build"
287    "preface.tex"
288    "root.tex"
289    "syntax.tex"
290
291session Logics_ZF (doc) in "Logics_ZF" = ZF +
292  options [document_variants = "logics-ZF", print_mode = "brackets",
293    thy_output_source]
294  sessions
295    FOL
296  theories
297    IFOL_examples
298    FOL_examples
299    ZF_examples
300    If
301    ZF_Isar
302  document_files (in "..")
303    "prepare_document"
304    "pdfsetup.sty"
305    "isar.sty"
306    "ttbox.sty"
307    "manual.bib"
308  document_files (in "../Logics/document")
309    "syntax.tex"
310  document_files
311    "FOL.tex"
312    "ZF.tex"
313    "build"
314    "logics.sty"
315    "root.tex"
316
317session Main (doc) in "Main" = HOL +
318  options [document_variants = "main"]
319  theories Main_Doc
320  document_files (in "..")
321    "prepare_document"
322    "pdfsetup.sty"
323  document_files
324    "build"
325    "root.tex"
326
327session Nitpick (doc) in "Nitpick" = Pure +
328  options [document_variants = "nitpick"]
329  document_files (in "..")
330    "prepare_document"
331    "pdfsetup.sty"
332    "iman.sty"
333    "manual.bib"
334  document_files
335    "build"
336    "root.tex"
337
338session Prog_Prove (doc) in "Prog_Prove" = HOL +
339  options [document_variants = "prog-prove", show_question_marks = false]
340  theories
341    Basics
342    Bool_nat_list
343    MyList
344    Types_and_funs
345    Logic
346    Isar
347  document_files (in ".")
348    "MyList.thy"
349  document_files (in "..")
350    "prepare_document"
351    "pdfsetup.sty"
352  document_files
353    "bang.pdf"
354    "build"
355    "intro-isabelle.tex"
356    "mathpartir.sty"
357    "prelude.tex"
358    "root.bib"
359    "root.tex"
360    "svmono.cls"
361
362session Sledgehammer (doc) in "Sledgehammer" = Pure +
363  options [document_variants = "sledgehammer"]
364  document_files (in "..")
365    "prepare_document"
366    "pdfsetup.sty"
367    "iman.sty"
368    "manual.bib"
369  document_files
370    "build"
371    "root.tex"
372
373session System (doc) in "System" = Pure +
374  options [document_variants = "system", thy_output_source]
375  sessions
376    "HOL-Library"
377  theories
378    Environment
379    Sessions
380    Presentation
381    Server
382    Scala
383    Misc
384  document_files (in "..")
385    "prepare_document"
386    "pdfsetup.sty"
387    "iman.sty"
388    "extra.sty"
389    "isar.sty"
390    "ttbox.sty"
391    "underscore.sty"
392    "manual.bib"
393  document_files (in "../Isar_Ref/document")
394    "style.sty"
395  document_files
396    "build"
397    "root.tex"
398
399session Tutorial (doc) in "Tutorial" = HOL +
400  options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
401  theories [threads = 1]
402    "ToyList/ToyList_Test"
403  theories [thy_output_indent = 5]
404    "ToyList/ToyList"
405    "Ifexpr/Ifexpr"
406    "CodeGen/CodeGen"
407    "Trie/Trie"
408    "Datatype/ABexpr"
409    "Datatype/unfoldnested"
410    "Datatype/Nested"
411    "Datatype/Fundata"
412    "Fun/fun0"
413    "Advanced/simp2"
414    "CTL/PDL"
415    "CTL/CTL"
416    "CTL/CTLind"
417    "Inductive/Even"
418    "Inductive/Mutual"
419    "Inductive/Star"
420    "Inductive/AB"
421    "Inductive/Advanced"
422    "Misc/Tree"
423    "Misc/Tree2"
424    "Misc/Plus"
425    "Misc/case_exprs"
426    "Misc/fakenat"
427    "Misc/natsum"
428    "Misc/pairs2"
429    "Misc/Option2"
430    "Misc/types"
431    "Misc/prime_def"
432    "Misc/simp"
433    "Misc/Itrev"
434    "Misc/AdvancedInd"
435    "Misc/appendix"
436  theories
437    "Protocol/NS_Public"
438    "Documents/Documents"
439  theories [document = false]
440    "Types/Setup"
441  theories [thy_output_margin = 64, thy_output_indent = 0]
442    "Types/Numbers"
443    "Types/Pairs"
444    "Types/Records"
445    "Types/Typedefs"
446    "Types/Overloading"
447    "Types/Axioms"
448    "Rules/Basic"
449    "Rules/Blast"
450    "Rules/Force"
451  theories [thy_output_margin = 64, thy_output_indent = 5]
452    "Rules/TPrimes"
453    "Rules/Forward"
454    "Rules/Tacticals"
455    "Rules/find2"
456    "Sets/Examples"
457    "Sets/Functions"
458    "Sets/Relations"
459    "Sets/Recur"
460  document_files (in "ToyList")
461    "ToyList1.txt"
462    "ToyList2.txt"
463  document_files (in "..")
464    "pdfsetup.sty"
465    "ttbox.sty"
466    "manual.bib"
467  document_files
468    "advanced0.tex"
469    "appendix0.tex"
470    "basics.tex"
471    "build"
472    "cl2emono-modified.sty"
473    "ctl0.tex"
474    "documents0.tex"
475    "fp.tex"
476    "inductive0.tex"
477    "isa-index"
478    "Isa-logics.pdf"
479    "numerics.tex"
480    "pghead.pdf"
481    "preface.tex"
482    "protocol.tex"
483    "root.tex"
484    "rules.tex"
485    "sets.tex"
486    "tutorial.sty"
487    "typedef.pdf"
488    "types0.tex"
489
490session Typeclass_Hierarchy (doc) in "Typeclass_Hierarchy" = "Typeclass_Hierarchy_Basics" +
491  options [document_variants = "typeclass_hierarchy"]
492  theories Typeclass_Hierarchy
493  document_files (in "..")
494    "prepare_document"
495    "pdfsetup.sty"
496    "iman.sty"
497    "extra.sty"
498    "isar.sty"
499    "manual.bib"
500  document_files
501    "build"
502    "root.tex"
503    "style.sty"
504
505session Typeclass_Hierarchy_Basics in "Typeclass_Hierarchy" = "HOL-Library" +
506  theories
507    Setup
508