Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
drop redundant fundef_cong rule
authorLars Hupel <lars.hupel@mytum.de>
Mon, 22 Jan 2018 16:08:50 +0100
changeset 67487 b4e65cd6974a
parent 67486 d617e84bb2b1
child 67488 3d33847dc911
drop redundant fundef_cong rule
src/HOL/Fun_Def.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Fun_Def.thy	Mon Jan 22 15:50:29 2018 +0100
+++ b/src/HOL/Fun_Def.thy	Mon Jan 22 16:08:50 2018 +0100
@@ -133,7 +133,7 @@
   unfolding Let_def by blast
 
 lemmas [fundef_cong] =
-  if_cong image_cong INF_cong SUP_cong
+  if_cong image_cong
   bex_cong ball_cong imp_cong map_option_cong Option.bind_cong
 
 lemma split_cong [fundef_cong]:
isabelle