author | huffman |
Thu, 19 Apr 2012 19:36:09 +0200 | |
changeset 47612 | bc9c7b5c26fd |
parent 47611 | e3c699a1fae6 |
child 47614 | 540a5af9a01c |
--- a/src/HOL/Transfer.thy Thu Apr 19 19:32:30 2012 +0200 +++ b/src/HOL/Transfer.thy Thu Apr 19 19:36:09 2012 +0200 @@ -234,6 +234,9 @@ lemma If_parametric [transfer_rule]: "(op = ===> A ===> A ===> A) If If" unfolding fun_rel_def by simp +lemma Let_parametric [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let" + unfolding fun_rel_def by simp + lemma comp_parametric [transfer_rule]: "((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \<circ>) (op \<circ>)" unfolding fun_rel_def by simp