# HG changeset patch # User huffman # Date 1334928613 -7200 # Node ID 10cfaf77168799262f6076202003a5befef96e88 # Parent 16d433895d2e4cf842bcf7e7c4e2d274bcf441dc add transfer rule for 'id' diff -r 16d433895d2e -r 10cfaf771687 src/HOL/Transfer.thy --- 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 \) (op \)" unfolding fun_rel_def by simp