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