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