src/HOL/Library/Permutation.thy
changeset 56154 f0a927235162
parent 55584 a879f14b6f95
child 56796 9f84219715a7
     1.1 --- a/src/HOL/Library/Permutation.thy	Sat Mar 15 03:37:22 2014 +0100
     1.2 +++ b/src/HOL/Library/Permutation.thy	Sat Mar 15 08:31:33 2014 +0100
     1.3 @@ -211,7 +211,7 @@
     1.4      proof (rule bij_betw_combine)
     1.5        show "bij_betw ?f (Suc ` {..<length xs}) (Suc ` {..<length ys})"
     1.6          using bij unfolding bij_betw_def
     1.7 -        by (auto intro!: inj_onI imageI dest: inj_onD simp: image_compose[symmetric] comp_def)
     1.8 +        by (auto intro!: inj_onI imageI dest: inj_onD simp: image_comp comp_def)
     1.9      qed (auto simp: bij_betw_def)
    1.10      fix i
    1.11      assume "i < length (z#xs)"