# HG changeset patch
# User huffman
# Date 1143225001 -3600
# Node ID 4565e230e6eb44136c5cd231ef01215e9a758dc0
# Parent  72e149c9caebdb9c5102e2f7d90420508aafa642
lazy patterns in lambda abstractions

diff -r 72e149c9caeb -r 4565e230e6eb src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Fri Mar 24 15:59:16 2006 +0100
+++ b/src/HOLCF/Fixrec.thy	Fri Mar 24 19:30:01 2006 +0100
@@ -410,6 +410,10 @@
   "_as_pat x (_match p v)" <= "_match (as_pat p) (_args (_var x) v)"
   "_lazy_pat (_match p v)" <= "_match (lazy_pat p) v"
 
+text {* Lazy patterns in lambda abstractions *}
+translations
+  "_cabs (_lazy_pat p) r" == "run oo (_Case1 (_lazy_pat p) r)"
+
 lemma wild_pat [simp]: "branch wild_pat\<cdot>(unit_when\<cdot>r)\<cdot>x = return\<cdot>r"
 by (simp add: branch_def wild_pat_def)