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: