src/HOL/HOLCF/Cprod.thy

--- a/src/HOL/HOLCF/Cprod.thy	Thu Dec 08 09:10:54 2011 +0100
+++ b/src/HOL/HOLCF/Cprod.thy	Thu Dec 08 13:25:40 2011 +0100
@@ -31,6 +31,13 @@
 translations
   "\<Lambda>(CONST Pair x y). t" == "CONST csplit\<cdot>(\<Lambda> x y. t)"
 
+abbreviation
+  cfst :: "'a \<times> 'b \<rightarrow> 'a" where
+  "cfst \<equiv> Abs_cfun fst"
+
+abbreviation
+  csnd :: "'a \<times> 'b \<rightarrow> 'b" where
+  "csnd \<equiv> Abs_cfun snd"
 
 subsection {* Convert all lemmas to the continuous versions *}