# HG changeset patch # User huffman # Date 1323347140 -3600 # Node ID 3f07a7a911806b6d801f7fe0a845e5368ffaaa1b # Parent 192243fd94a503df4463f38e980a6dbc4f70d732 reinstate old functions cfst and csnd as abbreviations 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 *}