equal
deleted
inserted
replaced
17 *} |
17 *} |
18 options [quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0] |
18 options [quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0] |
19 sessions |
19 sessions |
20 "HOL-Library" |
20 "HOL-Library" |
21 theories |
21 theories |
22 "HOL-Library.Old_Datatype" |
22 "HOL-Library.Realizers" |
23 |
23 |
24 session "HOL-Library" (main timing) in Library = HOL + |
24 session "HOL-Library" (main timing) in Library = HOL + |
25 description {* |
25 description {* |
26 Classical Higher-order Logic -- batteries included. |
26 Classical Higher-order Logic -- batteries included. |
27 *} |
27 *} |
50 (*prototypic tools*) |
50 (*prototypic tools*) |
51 Predicate_Compile_Quickcheck |
51 Predicate_Compile_Quickcheck |
52 (*legacy tools*) |
52 (*legacy tools*) |
53 Old_Datatype |
53 Old_Datatype |
54 Old_Recdef |
54 Old_Recdef |
|
55 Realizers |
55 Refute |
56 Refute |
56 document_files "root.bib" "root.tex" |
57 document_files "root.bib" "root.tex" |
57 |
58 |
58 session "HOL-Analysis" (main timing) in Analysis = HOL + |
59 session "HOL-Analysis" (main timing) in Analysis = HOL + |
59 options [document_tags = "unimportant", |
60 options [document_tags = "unimportant", |