| author | Walther Neuper <neuper@ist.tugraz.at> |
| Sun, 14 Jul 2013 14:48:14 +0200 | |
| changeset 52056 | f5d9bceb4dc0 |
| parent 51441 | d2c60ada3ece |
| child 52534 | 03b586ee5930 |
| permissions | -rw-r--r-- |
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 "../iman.sty"
9 "../extra.sty"
10 "../isar.sty"
11 "../manual.bib"
12 "document/build"
13 "document/root.tex"
14 "document/style.sty"
16 session Codegen (doc) in "Codegen" = "HOL-Library" +
17 options [document_variants = "codegen", print_mode = "no_brackets,iff"]
18 theories [document = false] Setup
19 theories
20 Introduction
21 Foundations
22 Refinement
23 Inductive_Predicate
24 Evaluation
25 Adaptation
26 Further
27 files
28 "../prepare_document"
29 "../pdfsetup.sty"
30 "../iman.sty"
31 "../extra.sty"
32 "../isar.sty"
33 "../manual.bib"
34 "document/adapt.tex"
35 "document/architecture.tex"
36 "document/build"
37 "document/root.tex"
38 "document/style.sty"
40 session Functions (doc) in "Functions" = HOL +
41 options [document_variants = "functions"]
42 theories Functions
43 files
44 "../prepare_document"
45 "../pdfsetup.sty"
46 "../iman.sty"
47 "../extra.sty"
48 "../isar.sty"
49 "../manual.bib"
50 "document/build"
51 "document/conclusion.tex"
52 "document/intro.tex"
53 "document/mathpartir.sty"
54 "document/root.tex"
55 "document/style.sty"
57 session Intro (doc) in "Intro" = Pure +
58 options [document_variants = "intro"]
59 theories
60 files
61 "../prepare_document"
62 "../pdfsetup.sty"
63 "../iman.sty"
64 "../extra.sty"
65 "../ttbox.sty"
66 "../manual.bib"
67 "document/build"
68 "document/root.tex"
70 session IsarImplementation (doc) in "IsarImplementation" = HOL +
71 options [document_variants = "implementation"]
72 theories
73 Eq
74 Integration
75 Isar
76 Local_Theory
77 Logic
78 ML
79 Prelim
80 Proof
81 Syntax
82 Tactic
83 files
84 "../prepare_document"
85 "../pdfsetup.sty"
86 "../iman.sty"
87 "../extra.sty"
88 "../isar.sty"
89 "../ttbox.sty"
90 "../underscore.sty"
91 "../manual.bib"
92 "document/build"
93 "document/root.tex"
94 "document/style.sty"
96 session IsarRef (doc) in "IsarRef" = HOL +
97 options [document_variants = "isar-ref", quick_and_dirty, thy_output_source]
98 theories
99 Preface
100 Synopsis
101 Framework
102 First_Order_Logic
103 Outer_Syntax
104 Document_Preparation
105 Spec
106 Proof
107 Inner_Syntax
108 Misc
109 Generic
110 HOL_Specific
111 Quick_Reference
112 Symbols
113 ML_Tactic
114 files
115 "../prepare_document"
116 "../pdfsetup.sty"
117 "../iman.sty"
118 "../extra.sty"
119 "../isar.sty"
120 "../ttbox.sty"
121 "../underscore.sty"
122 "../manual.bib"
123 "document/build"
124 "document/isar-vm.eps"
125 "document/isar-vm.pdf"
126 "document/isar-vm.svg"
127 "document/root.tex"
128 "document/showsymbols"
129 "document/style.sty"
131 session LaTeXsugar (doc) in "LaTeXsugar" = HOL +
132 options [document_variants = "sugar"]
133 theories [document = ""]
134 "~~/src/HOL/Library/LaTeXsugar"
135 "~~/src/HOL/Library/OptionalSugar"
136 theories Sugar
137 files
138 "../prepare_document"
139 "../pdfsetup.sty"
140 "document/build"
141 "document/mathpartir.sty"
142 "document/root.bib"
143 "document/root.tex"
145 session Locales (doc) in "Locales" = HOL +
146 options [document_variants = "locales", pretty_margin = 65]
147 theories
148 Examples1
149 Examples2
150 Examples3
151 files
152 "../prepare_document"
153 "../pdfsetup.sty"
154 "document/build"
155 "document/root.tex"
157 session Logics (doc) in "Logics" = Pure +
158 options [document_variants = "logics"]
159 theories
160 files
161 "../prepare_document"
162 "../pdfsetup.sty"
163 "../iman.sty"
164 "../extra.sty"
165 "../ttbox.sty"
166 "../manual.bib"
167 "document/build"
168 "document/root.tex"
170 session "Logics-HOL" (doc) in "HOL" = Pure +
171 options [document_variants = "logics-HOL"]
172 theories
173 files
174 "../prepare_document"
175 "../pdfsetup.sty"
176 "../iman.sty"
177 "../extra.sty"
178 "../ttbox.sty"
179 "../manual.bib"
180 "../Logics/document/syntax.tex"
181 "document/build"
182 "document/root.tex"
184 session "Logics-ZF" (doc) in "ZF" = ZF +
185 options [document_variants = "logics-ZF", print_mode = "brackets",
186 thy_output_source]
187 theories
188 IFOL_examples
189 FOL_examples
190 ZF_examples
191 If
192 ZF_Isar
193 files
194 "../prepare_document"
195 "../pdfsetup.sty"
196 "../isar.sty"
197 "../ttbox.sty"
198 "../manual.bib"
199 "../Logics/document/syntax.tex"
200 "document/build"
201 "document/root.tex"
203 session Main (doc) in "Main" = HOL +
204 options [document_variants = "main"]
205 theories Main_Doc
206 files
207 "../prepare_document"
208 "../pdfsetup.sty"
209 "document/build"
210 "document/root.tex"
212 session Nitpick (doc) in "Nitpick" = Pure +
213 options [document_variants = "nitpick"]
214 theories
215 files
216 "../prepare_document"
217 "../pdfsetup.sty"
218 "../iman.sty"
219 "../manual.bib"
220 "document/build"
221 "document/root.tex"
223 session ProgProve (doc) in "ProgProve" = HOL +
224 options [document_variants = "prog-prove", show_question_marks = false]
225 theories
226 Basics
227 Bool_nat_list
228 MyList
229 Types_and_funs
230 Logic
231 Isar
232 files
233 "../prepare_document"
234 "../pdfsetup.sty"
235 "document/bang.eps"
236 "document/bang.pdf"
237 "document/build"
238 "document/intro-isabelle.tex"
239 "document/mathpartir.sty"
240 "document/prelude.tex"
241 "document/root.bib"
242 "document/root.tex"
243 "document/svmono.cls"
245 session Ref (doc) in "Ref" = Pure +
246 options [document_variants = "ref"]
247 theories
248 files
249 "../prepare_document"
250 "../pdfsetup.sty"
251 "../iman.sty"
252 "../extra.sty"
253 "../ttbox.sty"
254 "../manual.bib"
255 "document/build"
256 "document/root.tex"
257 "document/syntax.tex"
258 "document/thm.tex"
260 session Sledgehammer (doc) in "Sledgehammer" = Pure +
261 options [document_variants = "sledgehammer"]
262 theories
263 files
264 "../prepare_document"
265 "../pdfsetup.sty"
266 "../iman.sty"
267 "../manual.bib"
268 "document/build"
269 "document/root.tex"
271 session System (doc) in "System" = Pure +
272 options [document_variants = "system", thy_output_source]
273 theories
274 Basics
275 Interfaces
276 Sessions
277 Presentation
278 Scala
279 Misc
280 files
281 "../prepare_document"
282 "../IsarRef/document/style.sty"
283 "../pdfsetup.sty"
284 "../iman.sty"
285 "../extra.sty"
286 "../isar.sty"
287 "../ttbox.sty"
288 "../underscore.sty"
289 "../manual.bib"
290 "document/browser_screenshot.eps"
291 "document/browser_screenshot.png"
292 "document/build"
293 "document/root.tex"
295 session Tutorial (doc) in "Tutorial" = HOL +
296 options [document_variants = "tutorial", print_mode = "brackets"]
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"
333 theories [document = ""]
334 "Types/Setup"
335 theories [pretty_margin = 64, thy_output_indent = 0]
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"
345 theories [pretty_margin = 64, thy_output_indent = 5]
346 "Rules/Primes"
347 "Rules/Forward"
348 "Rules/Tacticals"
349 "Rules/find2"
350 "Sets/Examples"
351 "Sets/Functions"
352 "Sets/Relations"
353 "Sets/Recur"
354 files
355 "ToyList/ToyList1"
356 "ToyList/ToyList2"
357 "../pdfsetup.sty"
358 "../ttbox.sty"
359 "../manual.bib"
360 "document/advanced0.tex"
361 "document/appendix0.tex"
362 "document/basics.tex"
363 "document/build"
364 "document/cl2emono-modified.sty"
365 "document/ctl0.tex"
366 "document/documents0.tex"
367 "document/fp.tex"
368 "document/inductive0.tex"
369 "document/isa-index"
370 "document/Isa-logics.eps"
371 "document/Isa-logics.pdf"
372 "document/numerics.tex"
373 "document/pghead.eps"
374 "document/pghead.pdf"
375 "document/preface.tex"
376 "document/protocol.tex"
377 "document/root.tex"
378 "document/rules.tex"
379 "document/sets.tex"
380 "document/tutorial.sty"
381 "document/typedef.pdf"
382 "document/typedef.ps"
383 "document/types0.tex"