author | wenzelm |
Mon, 06 Aug 2012 11:59:09 +0200 | |
changeset 48690 | c1499b14b48c |
parent 48679 | 5741f2152f5e |
child 48721 | 866f6d5baf4c |
permissions | -rw-r--r-- |
48509 | 1 |
session HOL! (main) in "." = Pure + |
48338 | 2 |
description {* Classical Higher-order Logic *} |
3 |
options [document_graph] |
|
4 |
theories Complex_Main |
|
48481 | 5 |
files "document/root.bib" "document/root.tex" |
48338 | 6 |
|
7 |
session "HOL-Base"! in "." = Pure + |
|
8 |
description {* Raw HOL base, with minimal tools *} |
|
48470
7483aa690b4f
clarified "document" again, eliminated redundant "no_document";
wenzelm
parents:
48458
diff
changeset
|
9 |
options [document = false] |
48338 | 10 |
theories HOL |
11 |
||
12 |
session "HOL-Plain"! in "." = Pure + |
|
13 |
description {* HOL side-entry after bootstrap of many tools and packages *} |
|
48470
7483aa690b4f
clarified "document" again, eliminated redundant "no_document";
wenzelm
parents:
48458
diff
changeset
|
14 |
options [document = false] |
48338 | 15 |
theories Plain |
16 |
||
17 |
session "HOL-Main"! in "." = Pure + |
|
18 |
description {* HOL side-entry for Main only, without Complex_Main *} |
|
48470
7483aa690b4f
clarified "document" again, eliminated redundant "no_document";
wenzelm
parents:
48458
diff
changeset
|
19 |
options [document = false] |
48338 | 20 |
theories Main |
21 |
||
48512 | 22 |
session "HOL-Proofs"! in "." = Pure + |
48509 | 23 |
description {* HOL-Main with explicit proof terms *} |
48470
7483aa690b4f
clarified "document" again, eliminated redundant "no_document";
wenzelm
parents:
48458
diff
changeset
|
24 |
options [document = false, proofs = 2, parallel_proofs = 0] |
48338 | 25 |
theories Main |
26 |
||
48481 | 27 |
session Library = HOL + |
28 |
description {* Classical Higher-order Logic -- batteries included *} |
|
29 |
theories |
|
30 |
Library |
|
31 |
List_Prefix |
|
32 |
List_lexord |
|
33 |
Sublist_Order |
|
34 |
Product_Lattice |
|
35 |
Code_Char_chr |
|
36 |
Code_Char_ord |
|
37 |
Code_Integer |
|
38 |
Efficient_Nat |
|
48690 | 39 |
(*"Code_Prolog" FIXME cf. 76965c356d2a *) |
48481 | 40 |
Code_Real_Approx_By_Float |
41 |
Target_Numeral |
|
42 |
files "document/root.bib" "document/root.tex" |
|
43 |
||
44 |
session Hahn_Banach = HOL + |
|
45 |
description {* |
|
46 |
Author: Gertrud Bauer, TU Munich |
|
47 |
||
48 |
The Hahn-Banach theorem for real vector spaces. |
|
49 |
*} |
|
50 |
options [document_graph] |
|
51 |
theories Hahn_Banach |
|
52 |
files "document/root.bib" "document/root.tex" |
|
53 |
||
54 |
session Induct = HOL + |
|
55 |
theories [quick_and_dirty] |
|
56 |
Common_Patterns |
|
57 |
theories |
|
58 |
QuoDataType |
|
59 |
QuoNestedDataType |
|
60 |
Term |
|
61 |
SList |
|
62 |
ABexp |
|
63 |
Tree |
|
64 |
Ordinals |
|
65 |
Sigma_Algebra |
|
66 |
Comb |
|
67 |
PropLog |
|
68 |
Com |
|
69 |
files "document/root.tex" |
|
70 |
||
71 |
session IMP = HOL + |
|
72 |
options [document_graph] |
|
73 |
theories [document = false] |
|
74 |
"~~/src/HOL/ex/Interpretation_with_Defs" |
|
75 |
"~~/src/HOL/Library/While_Combinator" |
|
76 |
"~~/src/HOL/Library/Char_ord" |
|
77 |
"~~/src/HOL/Library/List_lexord" |
|
78 |
theories |
|
79 |
BExp |
|
80 |
ASM |
|
81 |
Small_Step |
|
82 |
Denotation |
|
83 |
Comp_Rev |
|
84 |
Poly_Types |
|
85 |
Sec_Typing |
|
86 |
Sec_TypingT |
|
87 |
Def_Ass_Sound_Big |
|
88 |
Def_Ass_Sound_Small |
|
89 |
Live |
|
90 |
Live_True |
|
91 |
Hoare_Examples |
|
92 |
VC |
|
93 |
HoareT |
|
94 |
Collecting1 |
|
95 |
Collecting_list |
|
96 |
Abs_Int_Tests |
|
97 |
Abs_Int1_parity |
|
98 |
Abs_Int1_const |
|
99 |
Abs_Int3 |
|
100 |
"Abs_Int_ITP/Abs_Int1_parity_ITP" |
|
101 |
"Abs_Int_ITP/Abs_Int1_const_ITP" |
|
102 |
"Abs_Int_ITP/Abs_Int3_ITP" |
|
103 |
"Abs_Int_Den/Abs_Int_den2" |
|
104 |
Procs_Dyn_Vars_Dyn |
|
105 |
Procs_Stat_Vars_Dyn |
|
106 |
Procs_Stat_Vars_Stat |
|
107 |
C_like |
|
108 |
OO |
|
109 |
Fold |
|
110 |
files "document/root.bib" "document/root.tex" |
|
111 |
||
112 |
session IMPP = HOL + |
|
113 |
description {* |
|
114 |
Author: David von Oheimb |
|
115 |
Copyright 1999 TUM |
|
116 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
117 |
options [document = false] |
48481 | 118 |
theories EvenOdd |
119 |
||
120 |
session Import = HOL + |
|
121 |
options [document_graph] |
|
122 |
theories HOL_Light_Maps |
|
123 |
theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import |
|
124 |
||
125 |
session Number_Theory = HOL + |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
126 |
options [document = false] |
48481 | 127 |
theories Number_Theory |
128 |
||
129 |
session Old_Number_Theory = HOL + |
|
130 |
options [document_graph] |
|
131 |
theories [document = false] |
|
132 |
"~~/src/HOL/Library/Infinite_Set" |
|
133 |
"~~/src/HOL/Library/Permutation" |
|
134 |
theories |
|
135 |
Fib |
|
136 |
Factorization |
|
137 |
Chinese |
|
138 |
WilsonRuss |
|
139 |
WilsonBij |
|
140 |
Quadratic_Reciprocity |
|
141 |
Primes |
|
142 |
Pocklington |
|
143 |
files "document/root.tex" |
|
144 |
||
145 |
session Hoare = HOL + |
|
146 |
theories Hoare |
|
147 |
files "document/root.bib" "document/root.tex" |
|
148 |
||
149 |
session Hoare_Parallel = HOL + |
|
150 |
options [document_graph] |
|
151 |
theories Hoare_Parallel |
|
152 |
files "document/root.bib" "document/root.tex" |
|
153 |
||
154 |
session Codegenerator_Test = "HOL-Library" + |
|
155 |
options [document = false, document_graph = false, browser_info = false] |
|
48624 | 156 |
theories Generate Generate_Pretty RBT_Set_Test |
48481 | 157 |
|
158 |
session Metis_Examples = HOL + |
|
159 |
description {* |
|
160 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
161 |
Author: Jasmin Blanchette, TU Muenchen |
|
162 |
||
163 |
Testing Metis and Sledgehammer. |
|
164 |
*} |
|
48679 | 165 |
options [timeout = 3600, document = false] |
48481 | 166 |
theories |
167 |
Abstraction |
|
168 |
Big_O |
|
169 |
Binary_Tree |
|
170 |
Clausification |
|
171 |
Message |
|
172 |
Proxies |
|
173 |
Tarski |
|
174 |
Trans_Closure |
|
175 |
Sets |
|
176 |
||
177 |
session Nitpick_Examples = HOL + |
|
178 |
description {* |
|
179 |
Author: Jasmin Blanchette, TU Muenchen |
|
180 |
Copyright 2009 |
|
181 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
182 |
options [document = false] |
48481 | 183 |
theories [quick_and_dirty] Nitpick_Examples |
184 |
||
185 |
session Algebra = HOL + |
|
186 |
description {* |
|
187 |
Author: Clemens Ballarin, started 24 September 1999 |
|
188 |
||
189 |
The Isabelle Algebraic Library. |
|
190 |
*} |
|
191 |
options [document_graph] |
|
192 |
theories [document = false] |
|
193 |
(* Preliminaries from set and number theory *) |
|
194 |
"~~/src/HOL/Library/FuncSet" |
|
195 |
"~~/src/HOL/Old_Number_Theory/Primes" |
|
196 |
"~~/src/HOL/Library/Binomial" |
|
197 |
"~~/src/HOL/Library/Permutation" |
|
198 |
theories |
|
199 |
(*** New development, based on explicit structures ***) |
|
200 |
(* Groups *) |
|
201 |
FiniteProduct (* Product operator for commutative groups *) |
|
202 |
Sylow (* Sylow's theorem *) |
|
203 |
Bij (* Automorphism Groups *) |
|
204 |
||
205 |
(* Rings *) |
|
206 |
Divisibility (* Rings *) |
|
207 |
IntRing (* Ideals and residue classes *) |
|
208 |
UnivPoly (* Polynomials *) |
|
209 |
theories [document = false] |
|
210 |
(*** Old development, based on axiomatic type classes ***) |
|
211 |
"abstract/Abstract" (*The ring theory*) |
|
212 |
"poly/Polynomial" (*The full theory*) |
|
213 |
files "document/root.bib" "document/root.tex" |
|
214 |
||
215 |
session Auth = HOL + |
|
216 |
options [document_graph] |
|
217 |
theories |
|
218 |
Auth_Shared |
|
219 |
Auth_Public |
|
220 |
"Smartcard/Auth_Smartcard" |
|
221 |
"Guard/Auth_Guard_Shared" |
|
222 |
"Guard/Auth_Guard_Public" |
|
223 |
files "document/root.tex" |
|
224 |
||
225 |
session UNITY = HOL + |
|
226 |
description {* |
|
227 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
228 |
Copyright 1998 University of Cambridge |
|
229 |
||
230 |
Verifying security protocols using UNITY. |
|
231 |
*} |
|
232 |
options [document_graph] |
|
233 |
theories [document = false] "../Auth/Public" |
|
234 |
theories |
|
235 |
(*Basic meta-theory*) |
|
236 |
"UNITY_Main" |
|
237 |
||
238 |
(*Simple examples: no composition*) |
|
239 |
"Simple/Deadlock" |
|
240 |
"Simple/Common" |
|
241 |
"Simple/Network" |
|
242 |
"Simple/Token" |
|
243 |
"Simple/Channel" |
|
244 |
"Simple/Lift" |
|
245 |
"Simple/Mutex" |
|
246 |
"Simple/Reach" |
|
247 |
"Simple/Reachability" |
|
248 |
||
249 |
(*Verifying security protocols using UNITY*) |
|
250 |
"Simple/NSP_Bad" |
|
251 |
||
252 |
(*Example of composition*) |
|
253 |
"Comp/Handshake" |
|
254 |
||
255 |
(*Universal properties examples*) |
|
256 |
"Comp/Counter" |
|
257 |
"Comp/Counterc" |
|
258 |
"Comp/Priority" |
|
259 |
||
260 |
"Comp/TimerArray" |
|
261 |
"Comp/Progress" |
|
262 |
||
263 |
"Comp/Alloc" |
|
264 |
"Comp/AllocImpl" |
|
265 |
"Comp/Client" |
|
266 |
||
267 |
(*obsolete*) |
|
268 |
"ELT" |
|
269 |
files "document/root.tex" |
|
270 |
||
271 |
session Unix = HOL + |
|
272 |
options [print_mode = "no_brackets,no_type_brackets"] |
|
273 |
theories Unix |
|
274 |
files "document/root.bib" "document/root.tex" |
|
275 |
||
276 |
session ZF = HOL + |
|
277 |
description {* *} |
|
278 |
theories MainZF Games |
|
279 |
files "document/root.tex" |
|
280 |
||
281 |
session Imperative_HOL = HOL + |
|
282 |
description {* *} |
|
283 |
options [document_graph, print_mode = "iff,no_brackets"] |
|
284 |
theories [document = false] |
|
285 |
"~~/src/HOL/Library/Countable" |
|
286 |
"~~/src/HOL/Library/Monad_Syntax" |
|
287 |
"~~/src/HOL/Library/Code_Natural" |
|
288 |
"~~/src/HOL/Library/LaTeXsugar" |
|
289 |
theories Imperative_HOL_ex |
|
290 |
files "document/root.bib" "document/root.tex" |
|
291 |
||
292 |
session Decision_Procs = HOL + |
|
48496
a7eed34cf219
added condition = ISABELLE_POLYML according to no-smlnj targets in IsaMakefile;
wenzelm
parents:
48493
diff
changeset
|
293 |
options [condition = ISABELLE_POLYML, document = false] |
48481 | 294 |
theories Decision_Procs |
295 |
||
296 |
session ex in "Proofs/ex" = "HOL-Proofs" + |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
297 |
options [document = false, proofs = 2, parallel_proofs = 0] |
48481 | 298 |
theories Hilbert_Classical |
299 |
||
300 |
session Extraction in "Proofs/Extraction" = "HOL-Proofs" + |
|
301 |
description {* Examples for program extraction in Higher-Order Logic *} |
|
48496
a7eed34cf219
added condition = ISABELLE_POLYML according to no-smlnj targets in IsaMakefile;
wenzelm
parents:
48493
diff
changeset
|
302 |
options [condition = ISABELLE_POLYML, proofs = 2, parallel_proofs = 0] |
48481 | 303 |
theories [document = false] |
304 |
"~~/src/HOL/Library/Efficient_Nat" |
|
305 |
"~~/src/HOL/Library/Monad_Syntax" |
|
306 |
"~~/src/HOL/Number_Theory/Primes" |
|
307 |
"~~/src/HOL/Number_Theory/UniqueFactorization" |
|
308 |
"~~/src/HOL/Library/State_Monad" |
|
309 |
theories |
|
310 |
Greatest_Common_Divisor |
|
311 |
Warshall |
|
312 |
Higman_Extraction |
|
313 |
Pigeonhole |
|
314 |
Euclid |
|
315 |
files "document/root.bib" "document/root.tex" |
|
316 |
||
317 |
session Lambda in "Proofs/Lambda" = "HOL-Proofs" + |
|
318 |
options [document_graph, print_mode = "no_brackets", proofs = 2, parallel_proofs = 0] |
|
319 |
theories [document = false] |
|
320 |
"~~/src/HOL/Library/Code_Integer" |
|
321 |
theories |
|
322 |
Eta |
|
323 |
StrongNorm |
|
324 |
Standardization |
|
325 |
WeakNorm |
|
326 |
files "document/root.bib" "document/root.tex" |
|
327 |
||
328 |
session Prolog = HOL + |
|
329 |
description {* |
|
330 |
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) |
|
331 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
332 |
options [document = false] |
48481 | 333 |
theories Test Type |
334 |
||
335 |
session MicroJava = HOL + |
|
336 |
options [document_graph] |
|
337 |
theories [document = false] "~~/src/HOL/Library/While_Combinator" |
|
338 |
theories MicroJava |
|
339 |
files |
|
340 |
"document/introduction.tex" |
|
341 |
"document/root.bib" |
|
342 |
"document/root.tex" |
|
343 |
||
48636 | 344 |
session "MicroJava-skip_proofs" in MicroJava = HOL + |
345 |
options [condition = ISABELLE_FULL_TEST, document = false, skip_proofs, quick_and_dirty] |
|
346 |
theories MicroJava |
|
347 |
||
48481 | 348 |
session NanoJava = HOL + |
349 |
options [document_graph] |
|
350 |
theories Example |
|
351 |
files "document/root.bib" "document/root.tex" |
|
352 |
||
353 |
session Bali = HOL + |
|
354 |
options [document_graph] |
|
355 |
theories |
|
356 |
AxExample |
|
357 |
AxSound |
|
358 |
AxCompl |
|
359 |
Trans |
|
360 |
files "document/root.tex" |
|
361 |
||
362 |
session IOA = HOL + |
|
363 |
description {* |
|
364 |
Author: Tobias Nipkow & Konrad Slind |
|
365 |
Copyright 1994 TU Muenchen |
|
366 |
||
367 |
The meta theory of I/O-Automata. |
|
368 |
||
369 |
@inproceedings{Nipkow-Slind-IOA, |
|
370 |
author={Tobias Nipkow and Konrad Slind}, |
|
371 |
title={{I/O} Automata in {Isabelle/HOL}}, |
|
372 |
booktitle={Proc.\ TYPES Workshop 1994}, |
|
373 |
publisher=Springer, |
|
374 |
series=LNCS, |
|
375 |
note={To appear}} |
|
376 |
ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz |
|
377 |
||
378 |
and |
|
379 |
||
380 |
@inproceedings{Mueller-Nipkow, |
|
381 |
author={Olaf M\"uller and Tobias Nipkow}, |
|
382 |
title={Combining Model Checking and Deduction for {I/O}-Automata}, |
|
383 |
booktitle={Proc.\ TACAS Workshop}, |
|
384 |
organization={Aarhus University, BRICS report}, |
|
385 |
year=1995} |
|
386 |
ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz |
|
387 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
388 |
options [document = false] |
48481 | 389 |
theories Solve |
390 |
||
391 |
session Lattice = HOL + |
|
392 |
description {* |
|
393 |
Author: Markus Wenzel, TU Muenchen |
|
394 |
||
395 |
Basic theory of lattices and orders. |
|
396 |
*} |
|
397 |
theories CompleteLattice |
|
398 |
files "document/root.tex" |
|
399 |
||
400 |
session ex = HOL + |
|
401 |
description {* Miscellaneous examples for Higher-Order Logic. *} |
|
48679 | 402 |
options [timeout = 3600, condition = ISABELLE_POLYML] |
48481 | 403 |
theories [document = false] |
404 |
"~~/src/HOL/Library/State_Monad" |
|
405 |
Code_Nat_examples |
|
406 |
"~~/src/HOL/Library/FuncSet" |
|
407 |
Eval_Examples |
|
408 |
Normalization_by_Evaluation |
|
409 |
Hebrew |
|
410 |
Chinese |
|
411 |
Serbian |
|
412 |
"~~/src/HOL/Library/FinFun_Syntax" |
|
413 |
theories |
|
414 |
Iff_Oracle |
|
415 |
Coercion_Examples |
|
416 |
Numeral_Representation |
|
417 |
Higher_Order_Logic |
|
418 |
Abstract_NAT |
|
419 |
Guess |
|
420 |
Binary |
|
421 |
Fundefs |
|
422 |
Induction_Schema |
|
423 |
LocaleTest2 |
|
424 |
Records |
|
425 |
While_Combinator_Example |
|
426 |
MonoidGroup |
|
427 |
BinEx |
|
428 |
Hex_Bin_Examples |
|
429 |
Antiquote |
|
430 |
Multiquote |
|
431 |
PER |
|
432 |
NatSum |
|
433 |
ThreeDivides |
|
434 |
Intuitionistic |
|
435 |
CTL |
|
436 |
Arith_Examples |
|
437 |
BT |
|
438 |
Tree23 |
|
439 |
MergeSort |
|
440 |
Lagrange |
|
441 |
Groebner_Examples |
|
442 |
MT |
|
443 |
Unification |
|
444 |
Primrec |
|
445 |
Tarski |
|
446 |
Classical |
|
447 |
Set_Theory |
|
448 |
Meson_Test |
|
449 |
Termination |
|
450 |
Coherent |
|
451 |
PresburgerEx |
|
452 |
ReflectionEx |
|
453 |
Sqrt |
|
454 |
Sqrt_Script |
|
455 |
Transfer_Ex |
|
456 |
Transfer_Int_Nat |
|
457 |
HarmonicSeries |
|
458 |
Refute_Examples |
|
459 |
Landau |
|
460 |
Execute_Choice |
|
461 |
Summation |
|
462 |
Gauge_Integration |
|
463 |
Dedekind_Real |
|
464 |
Quicksort |
|
465 |
Birthday_Paradox |
|
466 |
List_to_Set_Comprehension_Examples |
|
467 |
Seq |
|
468 |
Simproc_Tests |
|
469 |
Executable_Relation |
|
470 |
FinFunPred |
|
471 |
Set_Comprehension_Pointfree_Tests |
|
472 |
Parallel_Example |
|
473 |
theories SVC_Oracle |
|
48690 | 474 |
theories [condition = SVC_HOME] |
475 |
svc_test |
|
48481 | 476 |
theories [condition = ZCHAFF_HOME] |
477 |
(*requires zChaff (or some other reasonably fast SAT solver)*) |
|
478 |
Sudoku |
|
479 |
(* FIXME |
|
480 |
(*requires a proof-generating SAT solver (zChaff or MiniSAT)*) |
|
481 |
(*global side-effects ahead!*) |
|
482 |
try use_thy "SAT_Examples"; (* FIXME try!? (not really a proper test) *) |
|
483 |
*) |
|
484 |
files "document/root.bib" "document/root.tex" |
|
485 |
||
486 |
session Isar_Examples = HOL + |
|
487 |
description {* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *} |
|
488 |
theories [document = false] |
|
489 |
"~~/src/HOL/Library/Lattice_Syntax" |
|
490 |
"../Number_Theory/Primes" |
|
491 |
theories |
|
492 |
Basic_Logic |
|
493 |
Cantor |
|
494 |
Drinker |
|
495 |
Expr_Compiler |
|
496 |
Fibonacci |
|
497 |
Group |
|
498 |
Group_Context |
|
499 |
Group_Notepad |
|
500 |
Hoare_Ex |
|
501 |
Knaster_Tarski |
|
502 |
Mutilated_Checkerboard |
|
503 |
Nested_Datatype |
|
504 |
Peirce |
|
505 |
Puzzle |
|
506 |
Summation |
|
507 |
files |
|
508 |
"document/root.bib" |
|
509 |
"document/root.tex" |
|
510 |
"document/style.tex" |
|
511 |
||
512 |
session SET_Protocol = HOL + |
|
513 |
options [document_graph] |
|
514 |
theories [document = false] "~~/src/HOL/Library/Nat_Bijection" |
|
515 |
theories SET_Protocol |
|
516 |
files "document/root.tex" |
|
517 |
||
518 |
session Matrix_LP = HOL + |
|
519 |
options [document_graph] |
|
520 |
theories Cplex |
|
521 |
files "document/root.tex" |
|
522 |
||
48614
6004f4575645
renamed session TLA to HOL-TLA to avoid clash with AFP;
wenzelm
parents:
48598
diff
changeset
|
523 |
session TLA = HOL + |
48481 | 524 |
description {* The Temporal Logic of Actions *} |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
525 |
options [document = false] |
48481 | 526 |
theories TLA |
527 |
||
48614
6004f4575645
renamed session TLA to HOL-TLA to avoid clash with AFP;
wenzelm
parents:
48598
diff
changeset
|
528 |
session Inc in "TLA/Inc" = "HOL-TLA" + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
529 |
options [document = false] |
48481 | 530 |
theories Inc |
531 |
||
48614
6004f4575645
renamed session TLA to HOL-TLA to avoid clash with AFP;
wenzelm
parents:
48598
diff
changeset
|
532 |
session Buffer in "TLA/Buffer" = "HOL-TLA" + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
533 |
options [document = false] |
48481 | 534 |
theories DBuffer |
535 |
||
48614
6004f4575645
renamed session TLA to HOL-TLA to avoid clash with AFP;
wenzelm
parents:
48598
diff
changeset
|
536 |
session Memory in "TLA/Memory" = "HOL-TLA" + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
537 |
options [document = false] |
48481 | 538 |
theories MemoryImplementation |
539 |
||
540 |
session TPTP = HOL + |
|
541 |
description {* |
|
542 |
Author: Jasmin Blanchette, TU Muenchen |
|
543 |
Author: Nik Sultana, University of Cambridge |
|
544 |
Copyright 2011 |
|
545 |
||
546 |
TPTP-related extensions. |
|
547 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
548 |
options [document = false] |
48481 | 549 |
theories |
550 |
ATP_Theory_Export |
|
551 |
MaSh_Eval |
|
552 |
MaSh_Export |
|
553 |
TPTP_Interpret |
|
554 |
THF_Arith |
|
555 |
theories [proofs = 0] (* FIXME !? *) |
|
556 |
ATP_Problem_Import |
|
557 |
||
558 |
session Multivariate_Analysis = HOL + |
|
559 |
options [document_graph] |
|
560 |
theories |
|
561 |
Multivariate_Analysis |
|
562 |
Determinants |
|
563 |
files |
|
564 |
"Integration.certs" |
|
565 |
"document/root.tex" |
|
566 |
||
567 |
session "HOL-Probability"! in "Probability" = "HOL-Multivariate_Analysis" + |
|
48617 | 568 |
options [document_graph] |
48481 | 569 |
theories [document = false] |
570 |
"~~/src/HOL/Library/Countable" |
|
571 |
"~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits" |
|
572 |
"~~/src/HOL/Library/Permutation" |
|
573 |
theories |
|
574 |
Probability |
|
575 |
"ex/Dining_Cryptographers" |
|
576 |
"ex/Koepf_Duermuth_Countermeasure" |
|
577 |
files "document/root.tex" |
|
578 |
||
48509 | 579 |
session Nominal (main) = HOL + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
580 |
options [document = false] |
48481 | 581 |
theories Nominal |
582 |
||
583 |
session Examples in "Nominal/Examples" = "HOL-Nominal" + |
|
48679 | 584 |
options [timeout = 3600, condition = ISABELLE_POLYML, document = false] |
48481 | 585 |
theories Nominal_Examples |
586 |
theories [quick_and_dirty] VC_Condition |
|
587 |
||
588 |
session Word = HOL + |
|
589 |
options [document_graph] |
|
590 |
theories Word |
|
591 |
files "document/root.bib" "document/root.tex" |
|
592 |
||
593 |
session Examples in "Word/Examples" = "HOL-Word" + |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
594 |
options [document = false] |
48481 | 595 |
theories WordExamples |
596 |
||
597 |
session Statespace = HOL + |
|
598 |
theories StateSpaceEx |
|
599 |
files "document/root.tex" |
|
600 |
||
601 |
session NSA = HOL + |
|
602 |
options [document_graph] |
|
603 |
theories Hypercomplex |
|
604 |
files "document/root.tex" |
|
605 |
||
606 |
session Examples in "NSA/Examples" = "HOL-NSA" + |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
607 |
options [document = false] |
48481 | 608 |
theories NSPrimes |
609 |
||
610 |
session Mirabelle = HOL + |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
611 |
options [document = false] |
48481 | 612 |
theories Mirabelle_Test |
48589
fb446a780d50
separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;
wenzelm
parents:
48588
diff
changeset
|
613 |
|
fb446a780d50
separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;
wenzelm
parents:
48588
diff
changeset
|
614 |
session ex in "Mirabelle/ex" = "HOL-Mirabelle" + |
fb446a780d50
separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;
wenzelm
parents:
48588
diff
changeset
|
615 |
theories Ex |
48481 | 616 |
|
617 |
session SMT_Examples = "HOL-Word" + |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
618 |
options [document = false, quick_and_dirty] |
48481 | 619 |
theories |
620 |
SMT_Tests |
|
621 |
SMT_Examples |
|
622 |
SMT_Word_Examples |
|
623 |
files |
|
624 |
"SMT_Examples.certs" |
|
625 |
"SMT_Tests.certs" |
|
626 |
||
627 |
session "HOL-Boogie"! in "Boogie" = "HOL-Word" + |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
628 |
options [document = false] |
48481 | 629 |
theories Boogie |
630 |
||
631 |
session Examples in "Boogie/Examples" = "HOL-Boogie" + |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
632 |
options [document = false] |
48481 | 633 |
theories |
634 |
Boogie_Max_Stepwise |
|
635 |
Boogie_Max |
|
636 |
Boogie_Dijkstra |
|
637 |
VCC_Max |
|
638 |
files |
|
48493 | 639 |
"Boogie_Dijkstra.b2i" |
48481 | 640 |
"Boogie_Dijkstra.certs" |
48493 | 641 |
"Boogie_Max.b2i" |
48481 | 642 |
"Boogie_Max.certs" |
48493 | 643 |
"VCC_Max.b2i" |
48481 | 644 |
"VCC_Max.certs" |
645 |
||
646 |
session "HOL-SPARK"! in "SPARK" = "HOL-Word" + |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
647 |
options [document = false] |
48481 | 648 |
theories SPARK |
649 |
||
650 |
session Examples in "SPARK/Examples" = "HOL-SPARK" + |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
651 |
options [document = false] |
48481 | 652 |
theories |
653 |
"Gcd/Greatest_Common_Divisor" |
|
654 |
||
655 |
"Liseq/Longest_Increasing_Subsequence" |
|
656 |
||
657 |
"RIPEMD-160/F" |
|
658 |
"RIPEMD-160/Hash" |
|
659 |
"RIPEMD-160/K_L" |
|
660 |
"RIPEMD-160/K_R" |
|
661 |
"RIPEMD-160/R_L" |
|
662 |
"RIPEMD-160/Round" |
|
663 |
"RIPEMD-160/R_R" |
|
664 |
"RIPEMD-160/S_L" |
|
665 |
"RIPEMD-160/S_R" |
|
666 |
||
667 |
"Sqrt/Sqrt" |
|
668 |
files |
|
669 |
"Gcd/greatest_common_divisor/g_c_d.fdl" |
|
670 |
"Gcd/greatest_common_divisor/g_c_d.rls" |
|
671 |
"Gcd/greatest_common_divisor/g_c_d.siv" |
|
672 |
"Liseq/liseq/liseq_length.fdl" |
|
673 |
"Liseq/liseq/liseq_length.rls" |
|
674 |
"Liseq/liseq/liseq_length.siv" |
|
675 |
"RIPEMD-160/rmd/f.fdl" |
|
676 |
"RIPEMD-160/rmd/f.rls" |
|
677 |
"RIPEMD-160/rmd/f.siv" |
|
678 |
"RIPEMD-160/rmd/hash.fdl" |
|
679 |
"RIPEMD-160/rmd/hash.rls" |
|
680 |
"RIPEMD-160/rmd/hash.siv" |
|
681 |
"RIPEMD-160/rmd/k_l.fdl" |
|
682 |
"RIPEMD-160/rmd/k_l.rls" |
|
683 |
"RIPEMD-160/rmd/k_l.siv" |
|
684 |
"RIPEMD-160/rmd/k_r.fdl" |
|
685 |
"RIPEMD-160/rmd/k_r.rls" |
|
686 |
"RIPEMD-160/rmd/k_r.siv" |
|
687 |
"RIPEMD-160/rmd/r_l.fdl" |
|
688 |
"RIPEMD-160/rmd/r_l.rls" |
|
689 |
"RIPEMD-160/rmd/r_l.siv" |
|
690 |
"RIPEMD-160/rmd/round.fdl" |
|
691 |
"RIPEMD-160/rmd/round.rls" |
|
692 |
"RIPEMD-160/rmd/round.siv" |
|
693 |
"RIPEMD-160/rmd/r_r.fdl" |
|
694 |
"RIPEMD-160/rmd/r_r.rls" |
|
695 |
"RIPEMD-160/rmd/r_r.siv" |
|
696 |
"RIPEMD-160/rmd/s_l.fdl" |
|
697 |
"RIPEMD-160/rmd/s_l.rls" |
|
698 |
"RIPEMD-160/rmd/s_l.siv" |
|
699 |
"RIPEMD-160/rmd/s_r.fdl" |
|
700 |
"RIPEMD-160/rmd/s_r.rls" |
|
701 |
"RIPEMD-160/rmd/s_r.siv" |
|
702 |
||
703 |
session Manual in "SPARK/Manual" = "HOL-SPARK" + |
|
48486 | 704 |
options [show_question_marks = false] |
48481 | 705 |
theories |
706 |
Example_Verification |
|
707 |
VC_Principles |
|
708 |
Reference |
|
709 |
Complex_Types |
|
710 |
files |
|
711 |
"complex_types_app/initialize.fdl" |
|
712 |
"complex_types_app/initialize.rls" |
|
713 |
"complex_types_app/initialize.siv" |
|
714 |
"document/complex_types.ads" |
|
715 |
"document/complex_types_app.adb" |
|
716 |
"document/complex_types_app.ads" |
|
717 |
"document/Gcd.adb" |
|
718 |
"document/Gcd.ads" |
|
719 |
"document/intro.tex" |
|
720 |
"document/loop_invariant.adb" |
|
721 |
"document/loop_invariant.ads" |
|
722 |
"document/root.bib" |
|
723 |
"document/root.tex" |
|
724 |
"document/Simple_Gcd.adb" |
|
725 |
"document/Simple_Gcd.ads" |
|
726 |
"loop_invariant/proc1.fdl" |
|
727 |
"loop_invariant/proc1.rls" |
|
728 |
"loop_invariant/proc1.siv" |
|
729 |
"loop_invariant/proc2.fdl" |
|
730 |
"loop_invariant/proc2.rls" |
|
731 |
"loop_invariant/proc2.siv" |
|
732 |
"simple_greatest_common_divisor/g_c_d.fdl" |
|
733 |
"simple_greatest_common_divisor/g_c_d.rls" |
|
734 |
"simple_greatest_common_divisor/g_c_d.siv" |
|
735 |
||
736 |
session Mutabelle = HOL + |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
737 |
options [document = false] |
48481 | 738 |
theories MutabelleExtra |
739 |
||
740 |
session Quickcheck_Examples = HOL + |
|
48679 | 741 |
options [timeout = 3600, document = false] |
48588 | 742 |
theories |
48690 | 743 |
Quickcheck_Examples |
744 |
(* FIXME |
|
745 |
Quickcheck_Lattice_Examples |
|
746 |
Completeness |
|
747 |
Quickcheck_Interfaces |
|
748 |
Hotel_Example *) |
|
48598 | 749 |
theories [condition = ISABELLE_GHC] |
750 |
Quickcheck_Narrowing_Examples |
|
48588 | 751 |
|
752 |
session Quickcheck_Benchmark = HOL + |
|
48635 | 753 |
theories [condition = ISABELLE_FULL_TEST, quick_and_dirty] |
48618
1f7e068b4613
moved another larger quickcheck example to Quickcheck_Benchmark
bulwahn
parents:
48614
diff
changeset
|
754 |
Find_Unused_Assms_Examples |
1f7e068b4613
moved another larger quickcheck example to Quickcheck_Benchmark
bulwahn
parents:
48614
diff
changeset
|
755 |
Needham_Schroeder_No_Attacker_Example |
1f7e068b4613
moved another larger quickcheck example to Quickcheck_Benchmark
bulwahn
parents:
48614
diff
changeset
|
756 |
Needham_Schroeder_Guided_Attacker_Example |
48690 | 757 |
Needham_Schroeder_Unguided_Attacker_Example |
48481 | 758 |
|
759 |
session Quotient_Examples = HOL + |
|
760 |
description {* |
|
761 |
Author: Cezary Kaliszyk and Christian Urban |
|
762 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
763 |
options [document = false] |
48481 | 764 |
theories |
765 |
DList |
|
766 |
FSet |
|
767 |
Quotient_Int |
|
768 |
Quotient_Message |
|
769 |
Lift_FSet |
|
770 |
Lift_Set |
|
771 |
Lift_Fun |
|
772 |
Quotient_Rat |
|
773 |
Lift_DList |
|
774 |
||
775 |
session Predicate_Compile_Examples = HOL + |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
776 |
options [document = false] |
48690 | 777 |
theories |
48481 | 778 |
Examples |
779 |
Predicate_Compile_Tests |
|
48690 | 780 |
(* FIXME |
781 |
Predicate_Compile_Quickcheck_Examples -- should be added again soon (since 21-Oct-2010) *) |
|
48481 | 782 |
Specialisation_Examples |
48690 | 783 |
(* FIXME since 21-Jul-2011 |
784 |
Hotel_Example_Small_Generator |
|
785 |
IMP_1 |
|
786 |
IMP_2 |
|
787 |
IMP_3 |
|
788 |
IMP_4 *) |
|
789 |
theories [condition = "ISABELLE_SWIPL"] (* FIXME: *or* ISABELLE_YAP (??) *) |
|
790 |
Code_Prolog_Examples |
|
791 |
Context_Free_Grammar_Example |
|
792 |
Hotel_Example_Prolog |
|
793 |
Lambda_Example |
|
794 |
List_Examples |
|
795 |
theories [condition = "ISABELLE_SWIPL", quick_and_dirty] (* FIXME: *or* ISABELLE_YAP (??) *) |
|
796 |
Reg_Exp_Example |
|
48481 | 797 |
|
48509 | 798 |
session HOLCF! (main) = HOL + |
48338 | 799 |
description {* |
800 |
Author: Franz Regensburger |
|
801 |
Author: Brian Huffman |
|
802 |
||
803 |
HOLCF -- a semantic extension of HOL by the LCF logic. |
|
804 |
*} |
|
805 |
options [document_graph] |
|
48470
7483aa690b4f
clarified "document" again, eliminated redundant "no_document";
wenzelm
parents:
48458
diff
changeset
|
806 |
theories [document = false] |
48338 | 807 |
"~~/src/HOL/Library/Nat_Bijection" |
808 |
"~~/src/HOL/Library/Countable" |
|
48481 | 809 |
theories |
810 |
Plain_HOLCF |
|
811 |
Fixrec |
|
812 |
HOLCF |
|
813 |
files "document/root.tex" |
|
814 |
||
815 |
session Tutorial in "HOLCF/Tutorial" = HOLCF + |
|
816 |
theories |
|
817 |
Domain_ex |
|
818 |
Fixrec_ex |
|
819 |
New_Domain |
|
820 |
files "document/root.tex" |
|
821 |
||
822 |
session Library in "HOLCF/Library" = HOLCF + |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
823 |
options [document = false] |
48481 | 824 |
theories HOLCF_Library |
825 |
||
826 |
session IMP in "HOLCF/IMP" = HOLCF + |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
827 |
options [document = false] |
48481 | 828 |
theories HoareEx |
48338 | 829 |
files "document/root.tex" |
830 |
||
48481 | 831 |
session ex in "HOLCF/ex" = HOLCF + |
832 |
description {* Misc HOLCF examples *} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
833 |
options [document = false] |
48481 | 834 |
theories |
835 |
Dnat |
|
836 |
Dagstuhl |
|
837 |
Focus_ex |
|
838 |
Fix2 |
|
839 |
Hoare |
|
840 |
Concurrency_Monad |
|
841 |
Loop |
|
842 |
Powerdomain_ex |
|
843 |
Domain_Proofs |
|
844 |
Letrec |
|
845 |
Pattern_Match |
|
846 |
||
847 |
session FOCUS in "HOLCF/FOCUS" = HOLCF + |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
848 |
options [document = false] |
48481 | 849 |
theories |
850 |
Fstreams |
|
851 |
FOCUS |
|
852 |
Buffer_adm |
|
853 |
||
854 |
session IOA! in "HOLCF/IOA" = HOLCF + |
|
855 |
description {* |
|
856 |
Author: Olaf Mueller |
|
857 |
||
858 |
Formalization of a semantic model of I/O-Automata. |
|
859 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
860 |
options [document = false] |
48481 | 861 |
theories "meta_theory/Abstraction" |
862 |
||
863 |
session ABP in "HOLCF/IOA/ABP" = IOA + |
|
864 |
description {* |
|
865 |
Author: Olaf Mueller |
|
866 |
||
867 |
The Alternating Bit Protocol performed in I/O-Automata. |
|
868 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
869 |
options [document = false] |
48481 | 870 |
theories Correctness |
871 |
||
872 |
session NTP in "HOLCF/IOA/NTP" = IOA + |
|
873 |
description {* |
|
874 |
Author: Tobias Nipkow & Konrad Slind |
|
875 |
||
876 |
A network transmission protocol, performed in the |
|
877 |
I/O automata formalization by Olaf Mueller. |
|
878 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
879 |
options [document = false] |
48481 | 880 |
theories Correctness |
881 |
||
882 |
session Storage in "HOLCF/IOA/Storage" = IOA + |
|
883 |
description {* |
|
884 |
Author: Olaf Mueller |
|
885 |
||
886 |
Memory storage case study. |
|
887 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
888 |
options [document = false] |
48481 | 889 |
theories Correctness |
890 |
||
891 |
session ex in "HOLCF/IOA/ex" = IOA + |
|
892 |
description {* |
|
893 |
Author: Olaf Mueller |
|
894 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
895 |
options [document = false] |
48481 | 896 |
theories |
897 |
TrivEx |
|
898 |
TrivEx2 |
|
899 |
||
900 |
session Datatype_Benchmark = HOL + |
|
901 |
description {* Some rather large datatype examples (from John Harrison). *} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
902 |
options [document = false] |
48635 | 903 |
theories [condition = ISABELLE_FULL_TEST, timing] |
48481 | 904 |
Brackin |
905 |
Instructions |
|
906 |
SML |
|
907 |
Verilog |
|
908 |
||
909 |
session Record_Benchmark = HOL + |
|
910 |
description {* Some benchmark on large record. *} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
911 |
options [document = false] |
48635 | 912 |
theories [condition = ISABELLE_FULL_TEST, timing] |
48481 | 913 |
Record_Benchmark |
914 |