reinstate old functions cfst and csnd as abbreviations
authorhuffman
Thu, 08 Dec 2011 13:25:40 +0100
changeset 45786 3f07a7a91180
parent 45785 192243fd94a5
child 45787 9fcaf2557c59
reinstate old functions cfst and csnd as abbreviations
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 *}