24 Refinement |
25 Refinement |
25 Inductive_Predicate |
26 Inductive_Predicate |
26 Evaluation |
27 Evaluation |
27 Adaptation |
28 Adaptation |
28 Further |
29 Further |
29 files |
30 document_files (in "..") |
30 "../prepare_document" |
31 "prepare_document" |
31 "../pdfsetup.sty" |
32 "pdfsetup.sty" |
32 "../iman.sty" |
33 "iman.sty" |
33 "../extra.sty" |
34 "extra.sty" |
34 "../isar.sty" |
35 "isar.sty" |
35 "../manual.bib" |
36 "manual.bib" |
36 "document/build" |
37 document_files |
37 "document/root.tex" |
38 "build" |
38 "document/style.sty" |
39 "root.tex" |
|
40 "style.sty" |
39 |
41 |
40 session Datatypes (doc) in "Datatypes" = HOL + |
42 session Datatypes (doc) in "Datatypes" = HOL + |
41 options [document_variants = "datatypes"] |
43 options [document_variants = "datatypes"] |
42 theories [document = false] Setup |
44 theories [document = false] Setup |
43 theories Datatypes |
45 theories Datatypes |
44 files |
46 document_files (in "..") |
45 "../prepare_document" |
47 "prepare_document" |
46 "../pdfsetup.sty" |
48 "pdfsetup.sty" |
47 "../iman.sty" |
49 "iman.sty" |
48 "../extra.sty" |
50 "extra.sty" |
49 "../isar.sty" |
51 "isar.sty" |
50 "../manual.bib" |
52 "manual.bib" |
51 "document/build" |
53 document_files |
52 "document/root.tex" |
54 "build" |
53 "document/style.sty" |
55 "root.tex" |
|
56 "style.sty" |
54 |
57 |
55 session Functions (doc) in "Functions" = HOL + |
58 session Functions (doc) in "Functions" = HOL + |
56 options [document_variants = "functions", skip_proofs = false, quick_and_dirty] |
59 options [document_variants = "functions", skip_proofs = false, quick_and_dirty] |
57 theories Functions |
60 theories Functions |
58 files |
61 document_files (in "..") |
59 "../prepare_document" |
62 "prepare_document" |
60 "../pdfsetup.sty" |
63 "pdfsetup.sty" |
61 "../iman.sty" |
64 "iman.sty" |
62 "../extra.sty" |
65 "extra.sty" |
63 "../isar.sty" |
66 "isar.sty" |
64 "../manual.bib" |
67 "manual.bib" |
65 "document/build" |
68 document_files |
66 "document/conclusion.tex" |
69 "build" |
67 "document/intro.tex" |
70 "conclusion.tex" |
68 "document/mathpartir.sty" |
71 "intro.tex" |
69 "document/root.tex" |
72 "mathpartir.sty" |
70 "document/style.sty" |
73 "root.tex" |
|
74 "style.sty" |
71 |
75 |
72 session Intro (doc) in "Intro" = Pure + |
76 session Intro (doc) in "Intro" = Pure + |
73 options [document_variants = "intro"] |
77 options [document_variants = "intro"] |
74 theories |
78 theories |
75 files |
79 document_files (in "..") |
76 "../prepare_document" |
80 "prepare_document" |
77 "../pdfsetup.sty" |
81 "pdfsetup.sty" |
78 "../iman.sty" |
82 "iman.sty" |
79 "../extra.sty" |
83 "extra.sty" |
80 "../ttbox.sty" |
84 "ttbox.sty" |
81 "../manual.bib" |
85 "manual.bib" |
82 "document/build" |
86 document_files |
83 "document/root.tex" |
87 "advanced.tex" |
|
88 "build" |
|
89 "foundations.tex" |
|
90 "getting.tex" |
|
91 "root.tex" |
84 |
92 |
85 session Implementation (doc) in "Implementation" = "HOL-Proofs" + |
93 session Implementation (doc) in "Implementation" = "HOL-Proofs" + |
86 options [document_variants = "implementation"] |
94 options [document_variants = "implementation"] |
87 theories |
95 theories |
88 Eq |
96 Eq |
125 Generic |
134 Generic |
126 HOL_Specific |
135 HOL_Specific |
127 Quick_Reference |
136 Quick_Reference |
128 Symbols |
137 Symbols |
129 ML_Tactic |
138 ML_Tactic |
130 files |
139 document_files (in "..") |
131 "../prepare_document" |
140 "prepare_document" |
132 "../pdfsetup.sty" |
141 "pdfsetup.sty" |
133 "../iman.sty" |
142 "iman.sty" |
134 "../extra.sty" |
143 "extra.sty" |
135 "../isar.sty" |
144 "isar.sty" |
136 "../ttbox.sty" |
145 "ttbox.sty" |
137 "../underscore.sty" |
146 "underscore.sty" |
138 "../manual.bib" |
147 "manual.bib" |
139 "document/build" |
148 document_files |
140 "document/isar-vm.pdf" |
149 "build" |
141 "document/isar-vm.svg" |
150 "isar-vm.pdf" |
142 "document/root.tex" |
151 "isar-vm.svg" |
143 "document/showsymbols" |
152 "root.tex" |
144 "document/style.sty" |
153 "showsymbols" |
|
154 "style.sty" |
145 |
155 |
146 session JEdit (doc) in "JEdit" = HOL + |
156 session JEdit (doc) in "JEdit" = HOL + |
147 options [document_variants = "jedit", thy_output_source] |
157 options [document_variants = "jedit", thy_output_source] |
148 theories |
158 theories |
149 JEdit |
159 JEdit |
150 files |
160 document_files (in "..") |
151 "../Isar_Ref/document/style.sty" |
161 "extra.sty" |
152 "../extra.sty" |
162 "iman.sty" |
153 "../iman.sty" |
163 "isar.sty" |
154 "../isar.sty" |
164 "manual.bib" |
155 "../manual.bib" |
165 "pdfsetup.sty" |
156 "../pdfsetup.sty" |
166 "prepare_document" |
157 "../prepare_document" |
167 "ttbox.sty" |
158 "../ttbox.sty" |
168 "underscore.sty" |
159 "../underscore.sty" |
169 document_files (in "../Isar_Ref/document") |
160 "document/build" |
170 "style.sty" |
161 "document/isabelle-jedit.png" |
171 document_files |
162 "document/popup1.png" |
172 "auto-tools.png" |
163 "document/popup2.png" |
173 "build" |
164 "document/root.tex" |
174 "find.png" |
|
175 "isabelle-jedit.png" |
|
176 "output.png" |
|
177 "popup1.png" |
|
178 "popup2.png" |
|
179 "root.tex" |
|
180 "sledgehammer.png" |
165 |
181 |
166 session Sugar (doc) in "Sugar" = HOL + |
182 session Sugar (doc) in "Sugar" = HOL + |
167 options [document_variants = "sugar"] |
183 options [document_variants = "sugar"] |
168 theories [document = ""] |
184 theories [document = ""] |
169 "~~/src/HOL/Library/LaTeXsugar" |
185 "~~/src/HOL/Library/LaTeXsugar" |
170 "~~/src/HOL/Library/OptionalSugar" |
186 "~~/src/HOL/Library/OptionalSugar" |
171 theories Sugar |
187 theories Sugar |
172 files |
188 document_files (in "..") |
173 "../prepare_document" |
189 "prepare_document" |
174 "../pdfsetup.sty" |
190 "pdfsetup.sty" |
175 "document/build" |
191 document_files |
176 "document/mathpartir.sty" |
192 "build" |
177 "document/root.bib" |
193 "mathpartir.sty" |
178 "document/root.tex" |
194 "root.bib" |
|
195 "root.tex" |
179 |
196 |
180 session Locales (doc) in "Locales" = HOL + |
197 session Locales (doc) in "Locales" = HOL + |
181 options [document_variants = "locales", pretty_margin = 65, skip_proofs = false] |
198 options [document_variants = "locales", pretty_margin = 65, skip_proofs = false] |
182 theories |
199 theories |
183 Examples1 |
200 Examples1 |
184 Examples2 |
201 Examples2 |
185 Examples3 |
202 Examples3 |
186 files |
203 document_files (in "..") |
187 "../prepare_document" |
204 "prepare_document" |
188 "../pdfsetup.sty" |
205 "pdfsetup.sty" |
189 "document/build" |
206 document_files |
190 "document/root.tex" |
207 "build" |
|
208 "root.bib" |
|
209 "root.tex" |
191 |
210 |
192 session Logics (doc) in "Logics" = Pure + |
211 session Logics (doc) in "Logics" = Pure + |
193 options [document_variants = "logics"] |
212 options [document_variants = "logics"] |
194 theories |
213 theories |
195 files |
214 document_files (in "..") |
196 "../prepare_document" |
215 "prepare_document" |
197 "../pdfsetup.sty" |
216 "pdfsetup.sty" |
198 "../iman.sty" |
217 "iman.sty" |
199 "../extra.sty" |
218 "extra.sty" |
200 "../ttbox.sty" |
219 "ttbox.sty" |
201 "../manual.bib" |
220 "manual.bib" |
202 "document/CTT.tex" |
221 document_files |
203 "document/HOL.tex" |
222 "CTT.tex" |
204 "document/LK.tex" |
223 "HOL.tex" |
205 "document/Sequents.tex" |
224 "LK.tex" |
206 "document/build" |
225 "Sequents.tex" |
207 "document/preface.tex" |
226 "build" |
208 "document/root.tex" |
227 "preface.tex" |
209 "document/syntax.tex" |
228 "root.tex" |
|
229 "syntax.tex" |
210 |
230 |
211 session Logics_ZF (doc) in "Logics_ZF" = ZF + |
231 session Logics_ZF (doc) in "Logics_ZF" = ZF + |
212 options [document_variants = "logics-ZF", print_mode = "brackets", |
232 options [document_variants = "logics-ZF", print_mode = "brackets", |
213 thy_output_source] |
233 thy_output_source] |
214 theories |
234 theories |
215 IFOL_examples |
235 IFOL_examples |
216 FOL_examples |
236 FOL_examples |
217 ZF_examples |
237 ZF_examples |
218 If |
238 If |
219 ZF_Isar |
239 ZF_Isar |
220 files |
240 document_files (in "..") |
221 "../prepare_document" |
241 "prepare_document" |
222 "../pdfsetup.sty" |
242 "pdfsetup.sty" |
223 "../isar.sty" |
243 "isar.sty" |
224 "../ttbox.sty" |
244 "ttbox.sty" |
225 "../manual.bib" |
245 "manual.bib" |
226 "../Logics/document/syntax.tex" |
246 document_files (in "../Logics/document") |
227 "document/build" |
247 "syntax.tex" |
228 "document/root.tex" |
248 document_files |
|
249 "FOL.tex" |
|
250 "ZF.tex" |
|
251 "build" |
|
252 "logics.sty" |
|
253 "root.tex" |
229 |
254 |
230 session Main (doc) in "Main" = HOL + |
255 session Main (doc) in "Main" = HOL + |
231 options [document_variants = "main"] |
256 options [document_variants = "main"] |
232 theories Main_Doc |
257 theories Main_Doc |
233 files |
258 document_files (in "..") |
234 "../prepare_document" |
259 "prepare_document" |
235 "../pdfsetup.sty" |
260 "pdfsetup.sty" |
236 "document/build" |
261 document_files |
237 "document/root.tex" |
262 "build" |
|
263 "root.tex" |
238 |
264 |
239 session Nitpick (doc) in "Nitpick" = Pure + |
265 session Nitpick (doc) in "Nitpick" = Pure + |
240 options [document_variants = "nitpick"] |
266 options [document_variants = "nitpick"] |
241 theories |
267 theories |
242 files |
268 document_files (in "..") |
243 "../prepare_document" |
269 "prepare_document" |
244 "../pdfsetup.sty" |
270 "pdfsetup.sty" |
245 "../iman.sty" |
271 "iman.sty" |
246 "../manual.bib" |
272 "manual.bib" |
247 "document/build" |
273 document_files |
248 "document/root.tex" |
274 "build" |
|
275 "root.tex" |
249 |
276 |
250 session Prog_Prove (doc) in "Prog_Prove" = HOL + |
277 session Prog_Prove (doc) in "Prog_Prove" = HOL + |
251 options [document_variants = "prog-prove", show_question_marks = false] |
278 options [document_variants = "prog-prove", show_question_marks = false] |
252 theories |
279 theories |
253 Basics |
280 Basics |
254 Bool_nat_list |
281 Bool_nat_list |
255 MyList |
282 MyList |
256 Types_and_funs |
283 Types_and_funs |
257 Logic |
284 Logic |
258 Isar |
285 Isar |
259 files |
286 document_files (in ".") |
260 "../prepare_document" |
287 "MyList.thy" |
261 "../pdfsetup.sty" |
288 document_files (in "..") |
262 "document/bang.pdf" |
289 "prepare_document" |
263 "document/build" |
290 "pdfsetup.sty" |
264 "document/intro-isabelle.tex" |
291 document_files |
265 "document/mathpartir.sty" |
292 "bang.pdf" |
266 "document/prelude.tex" |
293 "build" |
267 "document/root.bib" |
294 "intro-isabelle.tex" |
268 "document/root.tex" |
295 "mathpartir.sty" |
269 "document/svmono.cls" |
296 "prelude.tex" |
|
297 "root.bib" |
|
298 "root.tex" |
|
299 "svmono.cls" |
270 |
300 |
271 session Sledgehammer (doc) in "Sledgehammer" = Pure + |
301 session Sledgehammer (doc) in "Sledgehammer" = Pure + |
272 options [document_variants = "sledgehammer"] |
302 options [document_variants = "sledgehammer"] |
273 theories |
303 theories |
274 files |
304 document_files (in "..") |
275 "../prepare_document" |
305 "prepare_document" |
276 "../pdfsetup.sty" |
306 "pdfsetup.sty" |
277 "../iman.sty" |
307 "iman.sty" |
278 "../manual.bib" |
308 "manual.bib" |
279 "document/build" |
309 document_files |
280 "document/root.tex" |
310 "build" |
|
311 "root.tex" |
281 |
312 |
282 session System (doc) in "System" = Pure + |
313 session System (doc) in "System" = Pure + |
283 options [document_variants = "system", thy_output_source] |
314 options [document_variants = "system", thy_output_source] |
284 theories |
315 theories |
285 Basics |
316 Basics |
286 Interfaces |
317 Interfaces |
287 Sessions |
318 Sessions |
288 Presentation |
319 Presentation |
289 Scala |
320 Scala |
290 Misc |
321 Misc |
291 files |
322 document_files (in "..") |
292 "../prepare_document" |
323 "prepare_document" |
293 "../Isar_Ref/document/style.sty" |
324 "pdfsetup.sty" |
294 "../pdfsetup.sty" |
325 "iman.sty" |
295 "../iman.sty" |
326 "extra.sty" |
296 "../extra.sty" |
327 "isar.sty" |
297 "../isar.sty" |
328 "ttbox.sty" |
298 "../ttbox.sty" |
329 "underscore.sty" |
299 "../underscore.sty" |
330 "manual.bib" |
300 "../manual.bib" |
331 document_files (in "../Isar_Ref/document") |
301 "document/browser_screenshot.png" |
332 "style.sty" |
302 "document/build" |
333 document_files |
303 "document/root.tex" |
334 "browser_screenshot.png" |
|
335 "build" |
|
336 "root.tex" |
304 |
337 |
305 session Tutorial (doc) in "Tutorial" = HOL + |
338 session Tutorial (doc) in "Tutorial" = HOL + |
306 options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false] |
339 options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false] |
307 theories [threads = 1] |
340 theories [threads = 1] |
308 "ToyList/ToyList_Test" |
341 "ToyList/ToyList_Test" |