equal
deleted
inserted
replaced
4 |
4 |
5 Top theory for HOLCF system. |
5 Top theory for HOLCF system. |
6 *) |
6 *) |
7 |
7 |
8 theory HOLCF |
8 theory HOLCF |
9 imports Sprod Ssum Up Lift Discrete One Tr |
9 imports Sprod Ssum Up Lift Discrete One Tr Domain |
10 begin |
10 begin |
11 |
11 |
12 text {* |
12 text {* |
13 Remove continuity lemmas from simp set, so continuity subgoals |
13 Remove continuity lemmas from simp set, so continuity subgoals |
14 are handled by the @{text cont_proc} simplifier procedure. |
14 are handled by the @{text cont_proc} simplifier procedure. |