get Library/Permutations.thy compiled and working again
authorhuffman
Tue Aug 16 07:06:54 2011 -0700 (2011-08-16)
changeset 4422778e033e8ba05
parent 44221 bff7f7afb2db
child 44228 5f974bead436
get Library/Permutations.thy compiled and working again
src/HOL/Library/Library.thy
src/HOL/Library/Permutations.thy
     1.1 --- a/src/HOL/Library/Library.thy	Tue Aug 16 12:06:49 2011 +0200
     1.2 +++ b/src/HOL/Library/Library.thy	Tue Aug 16 07:06:54 2011 -0700
     1.3 @@ -43,6 +43,7 @@
     1.4    OptionalSugar
     1.5    Option_ord
     1.6    Permutation
     1.7 +  Permutations
     1.8    Poly_Deriv
     1.9    Polynomial
    1.10    Preorder
     2.1 --- a/src/HOL/Library/Permutations.thy	Tue Aug 16 12:06:49 2011 +0200
     2.2 +++ b/src/HOL/Library/Permutations.thy	Tue Aug 16 07:06:54 2011 -0700
     2.3 @@ -593,7 +593,8 @@
     2.4  
     2.5  lemma permutation_inverse_works: assumes p: "permutation p"
     2.6    shows "inv p o p = id" "p o inv p = id"
     2.7 -using permutation_bijective[OF p] surj_iff bij_def inj_iff by auto
     2.8 +  using permutation_bijective [OF p]
     2.9 +  unfolding bij_def inj_iff surj_iff by auto
    2.10  
    2.11  lemma permutation_inverse_compose:
    2.12    assumes p: "permutation p" and q: "permutation q"