Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Transfer.thy
changeset 58448 a1d4e7473c98
parent 58444 ed95293f14b6
child 58821 11e226e8a095 
--- a/src/HOL/Transfer.thy	Thu Sep 25 16:35:54 2014 +0200
+++ b/src/HOL/Transfer.thy	Thu Sep 25 16:35:56 2014 +0200
@@ -449,8 +449,7 @@
   shows "((A ===> op =) ===> op =) Ex Ex"
   using assms unfolding bi_total_def rel_fun_def by fast
 
-lemma If_transfer [transfer_rule]: "(op = ===> A ===> A ===> A) If If"
-  unfolding rel_fun_def by simp
+declare If_transfer [transfer_rule]
 
 lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let"
   unfolding rel_fun_def by simp
isabelle