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"