1 chapter Doc |
1 chapter Doc |
2 |
2 |
3 session Classes (doc) in "Classes" = HOL + |
3 session Classes (doc) in "Classes" = HOL + |
4 options [document_logo = "Isar", document_bibliography, document_build = "build", |
4 options [document_logo = "Isar", document_bibliography, |
5 document_variants = "classes", quick_and_dirty] |
5 document_variants = "classes", quick_and_dirty] |
6 theories [document = false] Setup |
6 theories [document = false] Setup |
7 theories Classes |
7 theories Classes |
8 document_files (in "..") |
8 document_files (in "..") |
9 "prepare_document" |
9 "pdfsetup.sty" |
10 "pdfsetup.sty" |
10 "iman.sty" |
11 "iman.sty" |
11 "extra.sty" |
12 "extra.sty" |
12 "isar.sty" |
13 "isar.sty" |
13 "manual.bib" |
14 "manual.bib" |
14 document_files |
15 document_files |
|
16 "build" |
|
17 "root.tex" |
15 "root.tex" |
18 "style.sty" |
16 "style.sty" |
19 |
17 |
20 session Codegen (doc) in "Codegen" = HOL + |
18 session Codegen (doc) in "Codegen" = HOL + |
21 options [document_logo = "Isar", document_bibliography, document_build = "build", |
19 options [document_logo = "Isar", document_bibliography, document_build = "build", |
44 "build" |
42 "build" |
45 "root.tex" |
43 "root.tex" |
46 "style.sty" |
44 "style.sty" |
47 |
45 |
48 session Corec (doc) in "Corec" = Datatypes + |
46 session Corec (doc) in "Corec" = Datatypes + |
49 options [document_build = "build", document_bibliography, document_variants = "corec"] |
47 options [document_bibliography, document_variants = "corec"] |
50 theories |
48 theories |
51 Corec |
49 Corec |
52 document_files (in "..") |
50 document_files (in "..") |
53 "prepare_document" |
51 "pdfsetup.sty" |
54 "pdfsetup.sty" |
52 "iman.sty" |
55 "iman.sty" |
53 "extra.sty" |
56 "extra.sty" |
54 "isar.sty" |
57 "isar.sty" |
55 "manual.bib" |
58 "manual.bib" |
56 document_files |
59 document_files |
|
60 "build" |
|
61 "root.tex" |
57 "root.tex" |
62 "style.sty" |
58 "style.sty" |
63 |
59 |
64 session Datatypes (doc) in "Datatypes" = HOL + |
60 session Datatypes (doc) in "Datatypes" = HOL + |
65 options [document_build = "build", document_bibliography, document_variants = "datatypes"] |
61 options [document_bibliography, document_variants = "datatypes"] |
66 sessions |
62 sessions |
67 "HOL-Library" |
63 "HOL-Library" |
68 theories [document = false] |
64 theories [document = false] |
69 Setup |
65 Setup |
70 theories |
66 theories |
71 Datatypes |
67 Datatypes |
72 document_files (in "..") |
68 document_files (in "..") |
73 "prepare_document" |
69 "pdfsetup.sty" |
74 "pdfsetup.sty" |
70 "iman.sty" |
75 "iman.sty" |
71 "extra.sty" |
76 "extra.sty" |
72 "isar.sty" |
77 "isar.sty" |
73 "manual.bib" |
78 "manual.bib" |
74 document_files |
79 document_files |
|
80 "build" |
|
81 "root.tex" |
75 "root.tex" |
82 "style.sty" |
76 "style.sty" |
83 |
77 |
84 session Eisbach (doc) in "Eisbach" = HOL + |
78 session Eisbach (doc) in "Eisbach" = HOL + |
85 options [document_logo = "Eisbach", document_bibliography, document_build = "build", |
79 options [document_logo = "Eisbach", document_bibliography, document_variants = "eisbach", |
86 document_variants = "eisbach", quick_and_dirty, |
80 quick_and_dirty, print_mode = "no_brackets,iff", show_question_marks = false] |
87 print_mode = "no_brackets,iff", show_question_marks = false] |
|
88 sessions |
81 sessions |
89 "HOL-Eisbach" |
82 "HOL-Eisbach" |
90 theories [document = false] |
83 theories [document = false] |
91 Base |
84 Base |
92 theories |
85 theories |
93 Preface |
86 Preface |
94 Manual |
87 Manual |
95 document_files (in "..") |
88 document_files (in "..") |
96 "prepare_document" |
|
97 "pdfsetup.sty" |
89 "pdfsetup.sty" |
98 "iman.sty" |
90 "iman.sty" |
99 "extra.sty" |
91 "extra.sty" |
100 "isar.sty" |
92 "isar.sty" |
101 "ttbox.sty" |
93 "ttbox.sty" |
102 "underscore.sty" |
94 "underscore.sty" |
103 "manual.bib" |
95 "manual.bib" |
104 document_files |
96 document_files |
105 "build" |
|
106 "root.tex" |
97 "root.tex" |
107 "style.sty" |
98 "style.sty" |
108 |
99 |
109 session Functions (doc) in "Functions" = HOL + |
100 session Functions (doc) in "Functions" = HOL + |
110 options [document_build = "build", document_bibliography, document_variants = "functions", |
101 options [document_bibliography, document_variants = "functions", |
111 skip_proofs = false, quick_and_dirty] |
102 skip_proofs = false, quick_and_dirty] |
112 theories Functions |
103 theories Functions |
113 document_files (in "..") |
104 document_files (in "..") |
114 "prepare_document" |
105 "pdfsetup.sty" |
115 "pdfsetup.sty" |
106 "iman.sty" |
116 "iman.sty" |
107 "extra.sty" |
117 "extra.sty" |
108 "isar.sty" |
118 "isar.sty" |
109 "manual.bib" |
119 "manual.bib" |
110 document_files |
120 document_files |
|
121 "build" |
|
122 "conclusion.tex" |
111 "conclusion.tex" |
123 "intro.tex" |
112 "intro.tex" |
124 "root.tex" |
113 "root.tex" |
125 "style.sty" |
114 "style.sty" |
126 |
115 |
149 "foundations.tex" |
138 "foundations.tex" |
150 "getting.tex" |
139 "getting.tex" |
151 "root.tex" |
140 "root.tex" |
152 |
141 |
153 session Implementation (doc) in "Implementation" = HOL + |
142 session Implementation (doc) in "Implementation" = HOL + |
154 options [document_logo = "Isar", document_bibliography, document_build = "build", |
143 options [document_logo = "Isar", document_bibliography, |
155 document_variants = "implementation", quick_and_dirty] |
144 document_variants = "implementation", quick_and_dirty] |
156 theories |
145 theories |
157 Eq |
146 Eq |
158 Integration |
147 Integration |
159 Isar |
148 Isar |
164 Syntax |
153 Syntax |
165 Tactic |
154 Tactic |
166 theories [parallel_proofs = 0] |
155 theories [parallel_proofs = 0] |
167 Logic |
156 Logic |
168 document_files (in "..") |
157 document_files (in "..") |
169 "prepare_document" |
|
170 "pdfsetup.sty" |
158 "pdfsetup.sty" |
171 "iman.sty" |
159 "iman.sty" |
172 "extra.sty" |
160 "extra.sty" |
173 "isar.sty" |
161 "isar.sty" |
174 "ttbox.sty" |
162 "ttbox.sty" |
175 "underscore.sty" |
163 "underscore.sty" |
176 "manual.bib" |
164 "manual.bib" |
177 document_files |
165 document_files |
178 "build" |
|
179 "root.tex" |
166 "root.tex" |
180 "style.sty" |
167 "style.sty" |
181 |
168 |
182 session Isar_Ref (doc) in "Isar_Ref" = HOL + |
169 session Isar_Ref (doc) in "Isar_Ref" = HOL + |
183 options [document_logo = "Isar", document_bibliography, document_build = "build", |
170 options [document_logo = "Isar", document_bibliography, document_variants = "isar-ref", |
184 document_variants = "isar-ref", quick_and_dirty, thy_output_source] |
171 quick_and_dirty, thy_output_source] |
185 sessions |
172 sessions |
186 "HOL-Library" |
173 "HOL-Library" |
187 theories |
174 theories |
188 Preface |
175 Preface |
189 Synopsis |
176 Synopsis |
198 Generic |
185 Generic |
199 HOL_Specific |
186 HOL_Specific |
200 Quick_Reference |
187 Quick_Reference |
201 Symbols |
188 Symbols |
202 document_files (in "..") |
189 document_files (in "..") |
203 "prepare_document" |
|
204 "pdfsetup.sty" |
190 "pdfsetup.sty" |
205 "iman.sty" |
191 "iman.sty" |
206 "extra.sty" |
192 "extra.sty" |
207 "isar.sty" |
193 "isar.sty" |
208 "ttbox.sty" |
194 "ttbox.sty" |
209 "underscore.sty" |
195 "underscore.sty" |
210 "manual.bib" |
196 "manual.bib" |
211 document_files |
197 document_files |
212 "build" |
|
213 "isar-vm.pdf" |
198 "isar-vm.pdf" |
214 "isar-vm.svg" |
199 "isar-vm.svg" |
215 "root.tex" |
200 "root.tex" |
216 "style.sty" |
201 "style.sty" |
217 |
202 |
218 session JEdit (doc) in "JEdit" = HOL + |
203 session JEdit (doc) in "JEdit" = HOL + |
219 options [document_logo = "jEdit", document_bibliography, document_build = "build", |
204 options [document_logo = "jEdit", document_bibliography, document_variants = "jedit", |
220 document_variants = "jedit", thy_output_source] |
205 thy_output_source] |
221 theories |
206 theories |
222 JEdit |
207 JEdit |
223 document_files (in "..") |
208 document_files (in "..") |
224 "extra.sty" |
209 "extra.sty" |
225 "iman.sty" |
210 "iman.sty" |
226 "isar.sty" |
211 "isar.sty" |
227 "manual.bib" |
212 "manual.bib" |
228 "pdfsetup.sty" |
213 "pdfsetup.sty" |
229 "prepare_document" |
|
230 "ttbox.sty" |
214 "ttbox.sty" |
231 "underscore.sty" |
215 "underscore.sty" |
232 document_files (in "../Isar_Ref/document") |
216 document_files (in "../Isar_Ref/document") |
233 "style.sty" |
217 "style.sty" |
234 document_files |
218 document_files |
235 "auto-tools.png" |
219 "auto-tools.png" |
236 "bibtex-mode.png" |
220 "bibtex-mode.png" |
237 "build" |
|
238 "cite-completion.png" |
221 "cite-completion.png" |
239 "isabelle-jedit.png" |
222 "isabelle-jedit.png" |
240 "markdown-document.png" |
223 "markdown-document.png" |
241 "ml-debugger.png" |
224 "ml-debugger.png" |
242 "output-and-state.png" |
225 "output-and-state.png" |
252 "sidekick.png" |
235 "sidekick.png" |
253 "sledgehammer.png" |
236 "sledgehammer.png" |
254 "theories.png" |
237 "theories.png" |
255 |
238 |
256 session Sugar (doc) in "Sugar" = HOL + |
239 session Sugar (doc) in "Sugar" = HOL + |
257 options [document_build = "build", document_bibliography, document_variants = "sugar"] |
240 options [document_bibliography, document_variants = "sugar"] |
258 sessions |
241 sessions |
259 "HOL-Library" |
242 "HOL-Library" |
260 theories Sugar |
243 theories Sugar |
261 document_files (in "..") |
244 document_files (in "..") |
262 "prepare_document" |
245 "pdfsetup.sty" |
263 "pdfsetup.sty" |
246 document_files |
264 document_files |
|
265 "build" |
|
266 "root.bib" |
247 "root.bib" |
267 "root.tex" |
248 "root.tex" |
268 |
249 |
269 session Locales (doc) in "Locales" = HOL + |
250 session Locales (doc) in "Locales" = HOL + |
270 options [document_build = "build", document_bibliography, |
251 options [document_bibliography, document_variants = "locales", |
271 document_variants = "locales", thy_output_margin = 65, skip_proofs = false] |
252 thy_output_margin = 65, skip_proofs = false] |
272 theories |
253 theories |
273 Examples1 |
254 Examples1 |
274 Examples2 |
255 Examples2 |
275 Examples3 |
256 Examples3 |
276 document_files (in "..") |
257 document_files (in "..") |
277 "prepare_document" |
258 "pdfsetup.sty" |
278 "pdfsetup.sty" |
259 document_files |
279 document_files |
|
280 "build" |
|
281 "root.bib" |
260 "root.bib" |
282 "root.tex" |
261 "root.tex" |
283 |
262 |
284 session Logics (doc) in "Logics" = Pure + |
263 session Logics (doc) in "Logics" = Pure + |
285 options [document_logo = "_", document_bibliography, document_build = "build", |
264 options [document_logo = "_", document_bibliography, document_build = "build", |
334 "pdfsetup.sty" |
313 "pdfsetup.sty" |
335 document_files |
314 document_files |
336 "root.tex" |
315 "root.tex" |
337 |
316 |
338 session Nitpick (doc) in "Nitpick" = Pure + |
317 session Nitpick (doc) in "Nitpick" = Pure + |
339 options [document_logo = "Nitpick", document_bibliography, document_build = "build", |
318 options [document_logo = "Nitpick", document_bibliography, document_variants = "nitpick"] |
340 document_variants = "nitpick"] |
319 document_files (in "..") |
341 document_files (in "..") |
320 "pdfsetup.sty" |
342 "prepare_document" |
321 "iman.sty" |
343 "pdfsetup.sty" |
322 "manual.bib" |
344 "iman.sty" |
323 document_files |
345 "manual.bib" |
|
346 document_files |
|
347 "build" |
|
348 "root.tex" |
324 "root.tex" |
349 |
325 |
350 session Prog_Prove (doc) in "Prog_Prove" = HOL + |
326 session Prog_Prove (doc) in "Prog_Prove" = HOL + |
351 options [document_logo = "HOL", document_bibliography, document_build = "build", |
327 options [document_logo = "HOL", document_bibliography, document_variants = "prog-prove", |
352 document_variants = "prog-prove", show_question_marks = false] |
328 show_question_marks = false] |
353 theories |
329 theories |
354 Basics |
330 Basics |
355 Bool_nat_list |
331 Bool_nat_list |
356 MyList |
332 MyList |
357 Types_and_funs |
333 Types_and_funs |
358 Logic |
334 Logic |
359 Isar |
335 Isar |
360 document_files (in ".") |
336 document_files (in ".") |
361 "MyList.thy" |
337 "MyList.thy" |
362 document_files (in "..") |
338 document_files (in "..") |
363 "prepare_document" |
|
364 "pdfsetup.sty" |
339 "pdfsetup.sty" |
365 document_files |
340 document_files |
366 "bang.pdf" |
341 "bang.pdf" |
367 "build" |
|
368 "intro-isabelle.tex" |
342 "intro-isabelle.tex" |
369 "prelude.tex" |
343 "prelude.tex" |
370 "root.bib" |
344 "root.bib" |
371 "root.tex" |
345 "root.tex" |
372 "svmono.cls" |
346 "svmono.cls" |
373 |
347 |
374 session Sledgehammer (doc) in "Sledgehammer" = Pure + |
348 session Sledgehammer (doc) in "Sledgehammer" = Pure + |
375 options [document_logo = "S/H", document_bibliography, document_build = "build", |
349 options [document_logo = "S/H", document_bibliography, document_variants = "sledgehammer"] |
376 document_variants = "sledgehammer"] |
350 document_files (in "..") |
377 document_files (in "..") |
351 "pdfsetup.sty" |
378 "prepare_document" |
352 "iman.sty" |
379 "pdfsetup.sty" |
353 "manual.bib" |
380 "iman.sty" |
354 document_files |
381 "manual.bib" |
|
382 document_files |
|
383 "build" |
|
384 "root.tex" |
355 "root.tex" |
385 |
356 |
386 session System (doc) in "System" = Pure + |
357 session System (doc) in "System" = Pure + |
387 options [document_logo = "_", document_bibliography, document_build = "build", |
358 options [document_logo = "_", document_bibliography, document_variants = "system", |
388 document_variants = "system", thy_output_source] |
359 thy_output_source] |
389 sessions |
360 sessions |
390 "HOL-Library" |
361 "HOL-Library" |
391 theories |
362 theories |
392 Environment |
363 Environment |
393 Sessions |
364 Sessions |
395 Server |
366 Server |
396 Scala |
367 Scala |
397 Phabricator |
368 Phabricator |
398 Misc |
369 Misc |
399 document_files (in "..") |
370 document_files (in "..") |
400 "prepare_document" |
|
401 "pdfsetup.sty" |
371 "pdfsetup.sty" |
402 "iman.sty" |
372 "iman.sty" |
403 "extra.sty" |
373 "extra.sty" |
404 "isar.sty" |
374 "isar.sty" |
405 "ttbox.sty" |
375 "ttbox.sty" |
406 "underscore.sty" |
376 "underscore.sty" |
407 "manual.bib" |
377 "manual.bib" |
408 document_files (in "../Isar_Ref/document") |
378 document_files (in "../Isar_Ref/document") |
409 "style.sty" |
379 "style.sty" |
410 document_files |
380 document_files |
411 "build" |
|
412 "root.tex" |
381 "root.tex" |
413 |
382 |
414 session Tutorial (doc) in "Tutorial" = HOL + |
383 session Tutorial (doc) in "Tutorial" = HOL + |
415 options [document_logo = "HOL", document_bibliography, document_build = "build", |
384 options [document_logo = "HOL", document_bibliography, document_build = "build", |
416 document_variants = "tutorial", print_mode = "brackets", skip_proofs = false] |
385 document_variants = "tutorial", print_mode = "brackets", skip_proofs = false] |
504 "tutorial.sty" |
473 "tutorial.sty" |
505 "typedef.pdf" |
474 "typedef.pdf" |
506 "types0.tex" |
475 "types0.tex" |
507 |
476 |
508 session Typeclass_Hierarchy (doc) in "Typeclass_Hierarchy" = HOL + |
477 session Typeclass_Hierarchy (doc) in "Typeclass_Hierarchy" = HOL + |
509 options [document_logo = "Isar", document_bibliography, document_build = "build", |
478 options [document_logo = "Isar", document_bibliography, document_variants = "typeclass_hierarchy"] |
510 document_variants = "typeclass_hierarchy"] |
|
511 sessions |
479 sessions |
512 "HOL-Library" |
480 "HOL-Library" |
513 theories [document = false] |
481 theories [document = false] |
514 Setup |
482 Setup |
515 theories |
483 theories |
516 Typeclass_Hierarchy |
484 Typeclass_Hierarchy |
517 document_files (in "..") |
485 document_files (in "..") |
518 "prepare_document" |
486 "pdfsetup.sty" |
519 "pdfsetup.sty" |
487 "iman.sty" |
520 "iman.sty" |
488 "extra.sty" |
521 "extra.sty" |
489 "isar.sty" |
522 "isar.sty" |
490 "manual.bib" |
523 "manual.bib" |
491 document_files |
524 document_files |
492 "root.tex" |
525 "build" |
493 "style.sty" |
526 "root.tex" |
|
527 "style.sty" |
|