# HG changeset patch
# User huffman
# Date 1130977702 -3600
# Node ID 9d4d70b175fd124dbd060d02bce0fe3b8ef584d5
# Parent  20e5a644079044d680d8e09f5e37153b44c7c99c
add translation for wildcard pattern

diff -r 20e5a6440790 -r 9d4d70b175fd src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Thu Nov 03 01:11:39 2005 +0100
+++ b/src/HOLCF/Cfun.thy	Thu Nov 03 01:28:22 2005 +0100
@@ -86,6 +86,9 @@
   in [("_cabs", cabs_ast_tr')] end;
 *}
 
+translations
+  "\<Lambda> _. t" == "Abs_CFun (\<lambda> _. t)"
+
 subsection {* Continuous function space is pointed *}
 
 lemma UU_CFun: "\<bottom> \<in> CFun"