equal
deleted
inserted
replaced
6 Lemmas for ssum3.thy |
6 Lemmas for ssum3.thy |
7 *) |
7 *) |
8 |
8 |
9 open Ssum3; |
9 open Ssum3; |
10 |
10 |
|
11 (* for compatibility with old HOLCF-Version *) |
|
12 qed_goal "inst_ssum_pcpo" thy "UU = Isinl UU" |
|
13 (fn prems => |
|
14 [ |
|
15 (simp_tac (HOL_ss addsimps [UU_def,UU_ssum_def]) 1) |
|
16 ]); |
|
17 |
11 (* ------------------------------------------------------------------------ *) |
18 (* ------------------------------------------------------------------------ *) |
12 (* continuity for Isinl and Isinr *) |
19 (* continuity for Isinl and Isinr *) |
13 (* ------------------------------------------------------------------------ *) |
20 (* ------------------------------------------------------------------------ *) |
14 |
|
15 |
21 |
16 qed_goal "contlub_Isinl" Ssum3.thy "contlub(Isinl)" |
22 qed_goal "contlub_Isinl" Ssum3.thy "contlub(Isinl)" |
17 (fn prems => |
23 (fn prems => |
18 [ |
24 [ |
19 (rtac contlubI 1), |
25 (rtac contlubI 1), |