src/HOL/Library/Permutation.thy
changeset 50037 f2a32197a33a
parent 44890 22f665a2e91c
child 51542 738598beeb26
     1.1 --- a/src/HOL/Library/Permutation.thy	Thu Nov 08 19:55:37 2012 +0100
     1.2 +++ b/src/HOL/Library/Permutation.thy	Thu Nov 08 20:02:41 2012 +0100
     1.3 @@ -193,7 +193,7 @@
     1.4    show ?case
     1.5    proof (intro exI[of _ "Fun.swap 0 1 id"] conjI allI impI)
     1.6      show "bij_betw (Fun.swap 0 1 id) {..<length (y # x # l)} {..<length (x # y # l)}"
     1.7 -      by (auto simp: bij_betw_def bij_betw_swap_iff)
     1.8 +      by (auto simp: bij_betw_def)
     1.9      fix i assume "i < length(y#x#l)"
    1.10      show "(y # x # l) ! i = (x # y # l) ! (Fun.swap 0 1 id) i"
    1.11        by (cases i) (auto simp: Fun.swap_def gr0_conv_Suc)