equal
deleted
inserted
replaced
4 |
4 |
5 HOLCF -- a semantic extension of HOL by the LCF logic. |
5 HOLCF -- a semantic extension of HOL by the LCF logic. |
6 *) |
6 *) |
7 |
7 |
8 theory HOLCF |
8 theory HOLCF |
9 imports Sprod Ssum Up Lift Discrete One Tr Domain ConvexPD Main |
9 imports Sprod Ssum Up Lift Discrete One Tr Domain ConvexPD Algebraic Universal Main |
10 uses |
10 uses |
11 "holcf_logic.ML" |
11 "holcf_logic.ML" |
12 "Tools/cont_consts.ML" |
12 "Tools/cont_consts.ML" |
13 "Tools/domain/domain_library.ML" |
13 "Tools/domain/domain_library.ML" |
14 "Tools/domain/domain_syntax.ML" |
14 "Tools/domain/domain_syntax.ML" |