Revert bij_betw changes to simp set (Problem in afp/Ordinals_and_Cardinals)
authorhoelzl
Thu Sep 02 21:08:31 2010 +0200 (2010-09-02)
changeset 39101606432dd1896
parent 39100 e9467adb8b52
child 39104 7430f17fd80e
Revert bij_betw changes to simp set (Problem in afp/Ordinals_and_Cardinals)
src/HOL/Fun.thy
     1.1 --- a/src/HOL/Fun.thy	Thu Sep 02 20:44:33 2010 +0200
     1.2 +++ b/src/HOL/Fun.thy	Thu Sep 02 21:08:31 2010 +0200
     1.3 @@ -177,7 +177,7 @@
     1.4  lemma surj_id[simp]: "surj_on id A"
     1.5  by (simp add: surj_on_def)
     1.6  
     1.7 -lemma bij_id[simp]: "bij_betw id A A"
     1.8 +lemma bij_id[simp]: "bij id"
     1.9  by (simp add: bij_betw_def)
    1.10  
    1.11  lemma inj_onI: