equal
deleted
inserted
replaced
36 Periodic_Fun |
36 Periodic_Fun |
37 Polynomial_Factorial |
37 Polynomial_Factorial |
38 Predicate_Compile_Quickcheck |
38 Predicate_Compile_Quickcheck |
39 Prefix_Order |
39 Prefix_Order |
40 Rewrite |
40 Rewrite |
41 Types_To_Sets |
|
42 (*conflicting type class instantiations*) |
41 (*conflicting type class instantiations*) |
43 List_lexord |
42 List_lexord |
44 Sublist_Order |
43 Sublist_Order |
45 Product_Lexorder |
44 Product_Lexorder |
46 Product_Order |
45 Product_Order |
1016 Lambda_Example |
1015 Lambda_Example |
1017 List_Examples |
1016 List_Examples |
1018 theories [condition = ISABELLE_SWIPL, quick_and_dirty] |
1017 theories [condition = ISABELLE_SWIPL, quick_and_dirty] |
1019 Reg_Exp_Example |
1018 Reg_Exp_Example |
1020 |
1019 |
|
1020 session "HOL-Types_To_Sets" in Types_To_Sets = HOL + |
|
1021 description {* |
|
1022 Experimental extension of Higher-Order Logic to allow translation of types to sets. |
|
1023 *} |
|
1024 options [document = false] |
|
1025 theories |
|
1026 Types_To_Sets |
|
1027 "Examples/Prerequisites" |
|
1028 "Examples/Finite" |
|
1029 "Examples/T2_Spaces" |
|
1030 |
1021 session HOLCF (main timing) in HOLCF = HOL + |
1031 session HOLCF (main timing) in HOLCF = HOL + |
1022 description {* |
1032 description {* |
1023 Author: Franz Regensburger |
1033 Author: Franz Regensburger |
1024 Author: Brian Huffman |
1034 Author: Brian Huffman |
1025 |
1035 |