src/HOL/Transfer.thy
changeset 47612 bc9c7b5c26fd
parent 47523 1bf0e92c1ca0
child 47618 1568dadd598a
     1.1 --- a/src/HOL/Transfer.thy	Thu Apr 19 19:32:30 2012 +0200
     1.2 +++ b/src/HOL/Transfer.thy	Thu Apr 19 19:36:09 2012 +0200
     1.3 @@ -234,6 +234,9 @@
     1.4  lemma If_parametric [transfer_rule]: "(op = ===> A ===> A ===> A) If If"
     1.5    unfolding fun_rel_def by simp
     1.6  
     1.7 +lemma Let_parametric [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let"
     1.8 +  unfolding fun_rel_def by simp
     1.9 +
    1.10  lemma comp_parametric [transfer_rule]:
    1.11    "((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \<circ>) (op \<circ>)"
    1.12    unfolding fun_rel_def by simp