1 chapter HOL |
1 chapter HOL |
2 |
2 |
3 session HOL (main) = Pure + |
3 session HOL (main) = Pure + |
4 description {* Classical Higher-order Logic *} |
4 description {* |
|
5 Classical Higher-order Logic. |
|
6 *} |
5 options [document_graph] |
7 options [document_graph] |
6 theories Complex_Main |
8 theories Complex_Main |
7 files |
9 files |
8 "Tools/Quickcheck/Narrowing_Engine.hs" |
10 "Tools/Quickcheck/Narrowing_Engine.hs" |
9 "Tools/Quickcheck/PNF_Narrowing_Engine.hs" |
11 "Tools/Quickcheck/PNF_Narrowing_Engine.hs" |
10 "document/root.bib" |
12 "document/root.bib" |
11 "document/root.tex" |
13 "document/root.tex" |
12 |
14 |
13 session "HOL-Proofs" = Pure + |
15 session "HOL-Proofs" = Pure + |
14 description {* HOL-Main with explicit proof terms *} |
16 description {* |
|
17 HOL-Main with explicit proof terms. |
|
18 *} |
15 options [document = false, proofs = 2] |
19 options [document = false, proofs = 2] |
16 theories Main |
20 theories Main |
17 files |
21 files |
18 "Tools/Quickcheck/Narrowing_Engine.hs" |
22 "Tools/Quickcheck/Narrowing_Engine.hs" |
19 "Tools/Quickcheck/PNF_Narrowing_Engine.hs" |
23 "Tools/Quickcheck/PNF_Narrowing_Engine.hs" |
20 |
24 |
21 session "HOL-Library" (main) in Library = HOL + |
25 session "HOL-Library" (main) in Library = HOL + |
22 description {* Classical Higher-order Logic -- batteries included *} |
26 description {* |
|
27 Classical Higher-order Logic -- batteries included. |
|
28 *} |
23 theories |
29 theories |
24 Library |
30 Library |
25 (*conflicting type class instantiations*) |
31 (*conflicting type class instantiations*) |
26 List_lexord |
32 List_lexord |
27 Sublist_Order |
33 Sublist_Order |
262 "abstract/Abstract" (*The ring theory*) |
268 "abstract/Abstract" (*The ring theory*) |
263 "poly/Polynomial" (*The full theory*) |
269 "poly/Polynomial" (*The full theory*) |
264 files "document/root.bib" "document/root.tex" |
270 files "document/root.bib" "document/root.tex" |
265 |
271 |
266 session "HOL-Auth" in Auth = HOL + |
272 session "HOL-Auth" in Auth = HOL + |
267 description {* A new approach to verifying authentication protocols. *} |
273 description {* |
|
274 A new approach to verifying authentication protocols. |
|
275 *} |
268 options [document_graph] |
276 options [document_graph] |
269 theories |
277 theories |
270 Auth_Shared |
278 Auth_Shared |
271 Auth_Public |
279 Auth_Public |
272 "Smartcard/Auth_Smartcard" |
280 "Smartcard/Auth_Smartcard" |
344 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" + |
352 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" + |
345 options [document = false, proofs = 2, parallel_proofs = 0] |
353 options [document = false, proofs = 2, parallel_proofs = 0] |
346 theories Hilbert_Classical |
354 theories Hilbert_Classical |
347 |
355 |
348 session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" + |
356 session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" + |
349 description {* Examples for program extraction in Higher-Order Logic *} |
357 description {* |
|
358 Examples for program extraction in Higher-Order Logic. |
|
359 *} |
350 options [condition = ISABELLE_POLYML, proofs = 2, parallel_proofs = 0] |
360 options [condition = ISABELLE_POLYML, proofs = 2, parallel_proofs = 0] |
351 theories [document = false] |
361 theories [document = false] |
352 "~~/src/HOL/Library/Code_Target_Numeral" |
362 "~~/src/HOL/Library/Code_Target_Numeral" |
353 "~~/src/HOL/Library/Monad_Syntax" |
363 "~~/src/HOL/Library/Monad_Syntax" |
354 "~~/src/HOL/Number_Theory/Primes" |
364 "~~/src/HOL/Number_Theory/Primes" |
469 *} |
479 *} |
470 theories CompleteLattice |
480 theories CompleteLattice |
471 files "document/root.tex" |
481 files "document/root.tex" |
472 |
482 |
473 session "HOL-ex" in ex = HOL + |
483 session "HOL-ex" in ex = HOL + |
474 description {* Miscellaneous examples for Higher-Order Logic. *} |
484 description {* |
|
485 Miscellaneous examples for Higher-Order Logic. |
|
486 *} |
475 options [timeout = 3600, condition = ISABELLE_POLYML] |
487 options [timeout = 3600, condition = ISABELLE_POLYML] |
476 theories [document = false] |
488 theories [document = false] |
477 "~~/src/HOL/Library/State_Monad" |
489 "~~/src/HOL/Library/State_Monad" |
478 Code_Binary_Nat_examples |
490 Code_Binary_Nat_examples |
479 "~~/src/HOL/Library/FuncSet" |
491 "~~/src/HOL/Library/FuncSet" |
667 options [timeout = 3600, condition = ISABELLE_POLYML, document = false] |
679 options [timeout = 3600, condition = ISABELLE_POLYML, document = false] |
668 theories Nominal_Examples |
680 theories Nominal_Examples |
669 theories [quick_and_dirty] VC_Condition |
681 theories [quick_and_dirty] VC_Condition |
670 |
682 |
671 session "HOL-Cardinals-Base" in Cardinals = HOL + |
683 session "HOL-Cardinals-Base" in Cardinals = HOL + |
672 description {* Ordinals and Cardinals, Base Theories *} |
684 description {* |
|
685 Ordinals and Cardinals, Base Theories. |
|
686 *} |
673 options [document = false] |
687 options [document = false] |
674 theories Cardinal_Arithmetic |
688 theories Cardinal_Arithmetic |
675 |
689 |
676 session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-Base" + |
690 session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-Base" + |
677 description {* Ordinals and Cardinals, Full Theories *} |
691 description {* |
|
692 Ordinals and Cardinals, Full Theories. |
|
693 *} |
678 options [document = false] |
694 options [document = false] |
679 theories Cardinals |
695 theories Cardinals |
680 files |
696 files |
681 "document/intro.tex" |
697 "document/intro.tex" |
682 "document/root.tex" |
698 "document/root.tex" |
683 "document/root.bib" |
699 "document/root.bib" |
684 |
700 |
685 session "HOL-BNF-LFP" in BNF = "HOL-Cardinals-Base" + |
701 session "HOL-BNF-LFP" in BNF = "HOL-Cardinals-Base" + |
686 description {* Bounded Natural Functors for Datatypes *} |
702 description {* |
|
703 Bounded Natural Functors for Datatypes. |
|
704 *} |
687 options [document = false] |
705 options [document = false] |
688 theories BNF_LFP |
706 theories BNF_LFP |
689 |
707 |
690 session "HOL-BNF" in BNF = "HOL-Cardinals" + |
708 session "HOL-BNF" in BNF = "HOL-Cardinals" + |
691 description {* Bounded Natural Functors for (Co)datatypes *} |
709 description {* |
|
710 Bounded Natural Functors for (Co)datatypes. |
|
711 *} |
692 options [document = false] |
712 options [document = false] |
693 theories BNF |
713 theories BNF |
694 |
714 |
695 session "HOL-BNF-Examples" in "BNF/Examples" = "HOL-BNF" + |
715 session "HOL-BNF-Examples" in "BNF/Examples" = "HOL-BNF" + |
696 description {* Examples for Bounded Natural Functors *} |
716 description {* |
|
717 Examples for Bounded Natural Functors. |
|
718 *} |
697 options [document = false] |
719 options [document = false] |
698 theories |
720 theories |
699 Lambda_Term |
721 Lambda_Term |
700 Process |
722 Process |
701 TreeFsetI |
723 TreeFsetI |
718 session "HOL-Statespace" in Statespace = HOL + |
740 session "HOL-Statespace" in Statespace = HOL + |
719 theories StateSpaceEx |
741 theories StateSpaceEx |
720 files "document/root.tex" |
742 files "document/root.tex" |
721 |
743 |
722 session "HOL-NSA" in NSA = HOL + |
744 session "HOL-NSA" in NSA = HOL + |
723 description {* Nonstandard analysis. *} |
745 description {* |
|
746 Nonstandard analysis. |
|
747 *} |
724 options [document_graph] |
748 options [document_graph] |
725 theories Hypercomplex |
749 theories Hypercomplex |
726 files "document/root.tex" |
750 files "document/root.tex" |
727 |
751 |
728 session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" + |
752 session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" + |
956 options [document = false] |
980 options [document = false] |
957 theories HoareEx |
981 theories HoareEx |
958 files "document/root.tex" |
982 files "document/root.tex" |
959 |
983 |
960 session "HOLCF-ex" in "HOLCF/ex" = HOLCF + |
984 session "HOLCF-ex" in "HOLCF/ex" = HOLCF + |
961 description {* Misc HOLCF examples *} |
985 description {* |
|
986 Miscellaneous examples for HOLCF. |
|
987 *} |
962 options [document = false] |
988 options [document = false] |
963 theories |
989 theories |
964 Dnat |
990 Dnat |
965 Dagstuhl |
991 Dagstuhl |
966 Focus_ex |
992 Focus_ex |
1044 theories |
1070 theories |
1045 TrivEx |
1071 TrivEx |
1046 TrivEx2 |
1072 TrivEx2 |
1047 |
1073 |
1048 session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL + |
1074 session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL + |
1049 description {* Some rather large datatype examples (from John Harrison). *} |
1075 description {* |
|
1076 Some rather large datatype examples (from John Harrison). |
|
1077 *} |
1050 options [document = false] |
1078 options [document = false] |
1051 theories [condition = ISABELLE_FULL_TEST, timing] |
1079 theories [condition = ISABELLE_FULL_TEST, timing] |
1052 Brackin |
1080 Brackin |
1053 Instructions |
1081 Instructions |
1054 SML |
1082 SML |
1055 Verilog |
1083 Verilog |
1056 |
1084 |
1057 session "HOL-Record_Benchmark" in Record_Benchmark = HOL + |
1085 session "HOL-Record_Benchmark" in Record_Benchmark = HOL + |
1058 description {* Some benchmark on large record. *} |
1086 description {* |
|
1087 Some benchmark on large record. |
|
1088 *} |
1059 options [document = false] |
1089 options [document = false] |
1060 theories [condition = ISABELLE_FULL_TEST, timing] |
1090 theories [condition = ISABELLE_FULL_TEST, timing] |
1061 Record_Benchmark |
1091 Record_Benchmark |
1062 |
1092 |