diff -r db9f95ca2a8f -r 313d3b697c9a src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Mon Apr 04 09:45:04 2016 +0200
+++ b/src/HOL/Fun.thy	Mon Apr 04 16:52:56 2016 +0100
@@ -36,6 +36,9 @@
 lemma vimage_id [simp]: "vimage id = id"
   by (simp add: id_def fun_eq_iff)
 
+lemma eq_id_iff: "(\<forall>x. f x = x) \<longleftrightarrow> f = id"
+  by auto
+
 code_printing
   constant id \<rightharpoonup> (Haskell) "id"