src/HOL/Fun.thy
changeset 39101 606432dd1896
parent 39076 b3a9b6734663
child 39198 f967a16dfcdd
--- a/src/HOL/Fun.thy	Thu Sep 02 20:44:33 2010 +0200
+++ b/src/HOL/Fun.thy	Thu Sep 02 21:08:31 2010 +0200
@@ -177,7 +177,7 @@
 lemma surj_id[simp]: "surj_on id A"
 by (simp add: surj_on_def)
 
-lemma bij_id[simp]: "bij_betw id A A"
+lemma bij_id[simp]: "bij id"
 by (simp add: bij_betw_def)
 
 lemma inj_onI: