--- a/src/HOLCF/Ssum3.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Ssum3.ML Mon Feb 17 10:57:11 1997 +0100
@@ -8,11 +8,17 @@
open Ssum3;
+(* for compatibility with old HOLCF-Version *)
+qed_goal "inst_ssum_pcpo" thy "UU = Isinl UU"
+ (fn prems =>
+ [
+ (simp_tac (HOL_ss addsimps [UU_def,UU_ssum_def]) 1)
+ ]);
+
(* ------------------------------------------------------------------------ *)
(* continuity for Isinl and Isinr *)
(* ------------------------------------------------------------------------ *)
-
qed_goal "contlub_Isinl" Ssum3.thy "contlub(Isinl)"
(fn prems =>
[