--- a/src/HOLCF/Cprod3.ML Wed Dec 18 15:12:34 1996 +0100
+++ b/src/HOLCF/Cprod3.ML Wed Dec 18 15:13:50 1996 +0100
@@ -228,6 +228,11 @@
(Simp_tac 1)
]);
+qed_goal "cfst_strict" Cprod3.thy "cfst`UU = UU" (fn _ => [
+ (simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,cfst2]) 1)]);
+qed_goal "csnd_strict" Cprod3.thy "csnd`UU = UU" (fn _ => [
+ (simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,csnd2]) 1)]);
+
qed_goalw "surjective_pairing_Cprod2" Cprod3.thy
[cfst_def,csnd_def,cpair_def] "<cfst`p , csnd`p> = p"
(fn prems =>