# HG changeset patch
# User oheimb
# Date 850918430 -3600
# Node ID 150644698367bb629b2fbddb838de7679d3b6a78
# Parent  a81d4c219c3c434380e7aa8cde44bb23a5b057d7
added cfst_strict and csnd_strict

diff -r a81d4c219c3c -r 150644698367 src/HOLCF/Cprod3.ML
--- 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 =>