changeset 16054 | b8ba6727712f |
parent 15742 | 64eae3513064 |
child 16841 | 228d663cc9b3 |
16053:603820cad083 | 16054:b8ba6727712f |
---|---|
7 |
7 |
8 theory HOLCF |
8 theory HOLCF |
9 imports Sprod Ssum Up Lift Discrete One Tr Domain |
9 imports Sprod Ssum Up Lift Discrete One Tr Domain |
10 begin |
10 begin |
11 |
11 |
12 text {* |
|
13 Remove continuity lemmas from simp set, so continuity subgoals |
|
14 are handled by the @{text cont_proc} simplifier procedure. |
|
15 *} |
|
16 declare cont_lemmas1 [simp del] |
|
17 declare cont_lemmas_ext [simp del] |
|
18 |
|
19 end |
12 end |