src/HOL/Hilbert_Choice.thy
changeset 49739 13aa6d8268ec
parent 48891 c0eafbd55de3
child 49948 744934b818c7
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Mon Oct 08 11:37:03 2012 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Mon Oct 08 12:03:49 2012 +0200
     1.3 @@ -144,7 +144,7 @@
     1.4  by (simp add: inj_iff)
     1.5  
     1.6  lemma o_inv_o_cancel[simp]: "inj f ==> g o inv f o f = g"
     1.7 -by (simp add: o_assoc[symmetric])
     1.8 +by (simp add: comp_assoc)
     1.9  
    1.10  lemma inv_into_image_cancel[simp]:
    1.11    "inj_on f A ==> S <= A ==> inv_into A f ` f ` S = S"