src/HOLCF/Fixrec.thy
changeset 19327 4565e230e6eb
parent 19104 7d69b6d7b8f1
child 19396 0592ea0c68a0
     1.1 --- a/src/HOLCF/Fixrec.thy	Fri Mar 24 15:59:16 2006 +0100
     1.2 +++ b/src/HOLCF/Fixrec.thy	Fri Mar 24 19:30:01 2006 +0100
     1.3 @@ -410,6 +410,10 @@
     1.4    "_as_pat x (_match p v)" <= "_match (as_pat p) (_args (_var x) v)"
     1.5    "_lazy_pat (_match p v)" <= "_match (lazy_pat p) v"
     1.6  
     1.7 +text {* Lazy patterns in lambda abstractions *}
     1.8 +translations
     1.9 +  "_cabs (_lazy_pat p) r" == "run oo (_Case1 (_lazy_pat p) r)"
    1.10 +
    1.11  lemma wild_pat [simp]: "branch wild_pat\<cdot>(unit_when\<cdot>r)\<cdot>x = return\<cdot>r"
    1.12  by (simp add: branch_def wild_pat_def)
    1.13