# HG changeset patch
# User huffman
# Date 1313503614 25200
# Node ID 78e033e8ba050a80ddead30a371b599d043aa8db
# Parent  bff7f7afb2db7c32646eb82b42c5191ecae7fa87
get Library/Permutations.thy compiled and working again

diff -r bff7f7afb2db -r 78e033e8ba05 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Tue Aug 16 12:06:49 2011 +0200
+++ b/src/HOL/Library/Library.thy	Tue Aug 16 07:06:54 2011 -0700
@@ -43,6 +43,7 @@
   OptionalSugar
   Option_ord
   Permutation
+  Permutations
   Poly_Deriv
   Polynomial
   Preorder
diff -r bff7f7afb2db -r 78e033e8ba05 src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Tue Aug 16 12:06:49 2011 +0200
+++ b/src/HOL/Library/Permutations.thy	Tue Aug 16 07:06:54 2011 -0700
@@ -593,7 +593,8 @@
 
 lemma permutation_inverse_works: assumes p: "permutation p"
   shows "inv p o p = id" "p o inv p = id"
-using permutation_bijective[OF p] surj_iff bij_def inj_iff by auto
+  using permutation_bijective [OF p]
+  unfolding bij_def inj_iff surj_iff by auto
 
 lemma permutation_inverse_compose:
   assumes p: "permutation p" and q: "permutation q"