# HG changeset patch
# User hoelzl
# Date 1283430848 -7200
# Node ID 39f8f6d1eb743692662836f42502e23e92eaadfa
# Parent  ee78849c16243b3c2843edc6cb5d90af627d8c77
Fixes lemma names

diff -r ee78849c1624 -r 39f8f6d1eb74 src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Thu Sep 02 13:32:17 2010 +0200
+++ b/src/HOL/Library/Permutation.thy	Thu Sep 02 14:34:08 2010 +0200
@@ -193,7 +193,7 @@
   show ?case
   proof (intro exI[of _ "Fun.swap 0 1 id"] conjI allI impI)
     show "bij_betw (Fun.swap 0 1 id) {..<length (y # x # l)} {..<length (x # y # l)}"
-      by (rule bij_betw_swap) (auto simp: bij_betw_def)
+      by (auto simp: bij_betw_def bij_betw_swap_iff)
     fix i assume "i < length(y#x#l)"
     show "(y # x # l) ! i = (x # y # l) ! (Fun.swap 0 1 id) i"
       by (cases i) (auto simp: Fun.swap_def gr0_conv_Suc)
@@ -207,7 +207,7 @@
   proof (intro exI[of _ ?f] allI conjI impI)
     have *: "{..<length (z#xs)} = {0} \<union> Suc ` {..<length xs}"
             "{..<length (z#ys)} = {0} \<union> Suc ` {..<length ys}"
-      by (simp_all add: lessThan_eq_Suc_image)
+      by (simp_all add: lessThan_Suc_eq_insert_0)
     show "bij_betw ?f {..<length (z#xs)} {..<length (z#ys)}" unfolding *
     proof (rule bij_betw_combine)
       show "bij_betw ?f (Suc ` {..<length xs}) (Suc ` {..<length ys})"