| changeset 35473 | c4d3d65856dd |
| parent 33588 | ea9becc59636 |
| child 35906 | e0382e4b4da7 |
| 35472:c23b42730b9b | 35473:c4d3d65856dd |
|---|---|
4 HOLCF -- a semantic extension of HOL by the LCF logic. |
4 HOLCF -- a semantic extension of HOL by the LCF logic. |
5 *) |
5 *) |
6 |
6 |
7 theory HOLCF |
7 theory HOLCF |
8 imports |
8 imports |
9 Domain ConvexPD Algebraic Universal Sum_Cpo Main |
9 Main |
10 Representable |
10 Domain |
11 Powerdomains |
|
12 Sum_Cpo |
|
11 uses |
13 uses |
12 "holcf_logic.ML" |
14 "holcf_logic.ML" |
13 "Tools/adm_tac.ML" |
15 "Tools/adm_tac.ML" |
14 begin |
16 begin |
15 |
17 |