equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* Domain package *} |
6 header {* Domain package *} |
7 |
7 |
8 theory Domain |
8 theory Domain |
9 imports Ssum Sprod One Up |
9 imports Ssum Sprod One Up Fixrec |
|
10 (* |
10 files |
11 files |
11 ("domain/library.ML") |
12 ("domain/library.ML") |
12 ("domain/syntax.ML") |
13 ("domain/syntax.ML") |
13 ("domain/axioms.ML") |
14 ("domain/axioms.ML") |
14 ("domain/theorems.ML") |
15 ("domain/theorems.ML") |
15 ("domain/extender.ML") |
16 ("domain/extender.ML") |
16 ("domain/interface.ML") |
17 ("domain/interface.ML") |
|
18 *) |
17 begin |
19 begin |
18 |
20 |
19 defaultsort pcpo |
21 defaultsort pcpo |
20 |
22 |
21 subsection {* Continuous isomorphisms *} |
23 subsection {* Continuous isomorphisms *} |