diff -r 192243fd94a5 -r 3f07a7a91180 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 "\(CONST Pair x y). t" == "CONST csplit\(\ x y. t)" +abbreviation + cfst :: "'a \ 'b \ 'a" where + "cfst \ Abs_cfun fst" + +abbreviation + csnd :: "'a \ 'b \ 'b" where + "csnd \ Abs_cfun snd" subsection {* Convert all lemmas to the continuous versions *}