author | huffman |
Thu, 08 Dec 2011 13:25:40 +0100 | |
changeset 45786 | 3f07a7a91180 |
parent 45785 | 192243fd94a5 |
child 45787 | 9fcaf2557c59 |
--- 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 *}