add transfer rule for Let
authorhuffman
Thu Apr 19 19:36:09 2012 +0200 (2012-04-19)
changeset 47612bc9c7b5c26fd
parent 47611 e3c699a1fae6
child 47614 540a5af9a01c
add transfer rule for Let
src/HOL/Transfer.thy
     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