src/HOL/Fun.thy
changeset 16733 236dfafbeb63
parent 15691 900cf45ff0a6
child 16973 b2a894562b8f
     1.1 --- a/src/HOL/Fun.thy	Thu Jul 07 12:36:56 2005 +0200
     1.2 +++ b/src/HOL/Fun.thy	Thu Jul 07 12:39:17 2005 +0200
     1.3 @@ -92,13 +92,16 @@
     1.4  lemma id_apply [simp]: "id x = x"
     1.5  by (simp add: id_def)
     1.6  
     1.7 -lemma inj_on_id: "inj_on id A"
     1.8 +lemma inj_on_id[simp]: "inj_on id A"
     1.9  by (simp add: inj_on_def) 
    1.10  
    1.11 -lemma surj_id: "surj id"
    1.12 +lemma inj_on_id2[simp]: "inj_on (%x. x) A"
    1.13 +by (simp add: inj_on_def) 
    1.14 +
    1.15 +lemma surj_id[simp]: "surj id"
    1.16  by (simp add: surj_def) 
    1.17  
    1.18 -lemma bij_id: "bij id"
    1.19 +lemma bij_id[simp]: "bij id"
    1.20  by (simp add: bij_def inj_on_id surj_id) 
    1.21  
    1.22