author | huffman |
Fri, 20 Apr 2012 15:30:13 +0200 | |
changeset 47625 | 10cfaf771687 |
parent 47624 | 16d433895d2e |
child 47626 | f7b1034cb9ce |
--- a/src/HOL/Transfer.thy Fri Apr 20 14:57:19 2012 +0200 +++ b/src/HOL/Transfer.thy Fri Apr 20 15:30:13 2012 +0200 @@ -240,6 +240,9 @@ lemma Let_parametric [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let" unfolding fun_rel_def by simp +lemma id_parametric [transfer_rule]: "(A ===> A) id id" + 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