src/HOL/Library/Permutations.thy
changeset 30074 38ce654e1b05
parent 30037 6ff7793d0f0d
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/Library/Permutations.thy	Mon Feb 23 07:58:13 2009 -0800
     1.2 +++ b/src/HOL/Library/Permutations.thy	Mon Feb 23 10:42:31 2009 -0800
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Permutations, both general and specifically on finite sets.*}
     1.5  
     1.6  theory Permutations
     1.7 -imports Main Finite_Cartesian_Product Parity 
     1.8 +imports Main Finite_Cartesian_Product Parity Fact
     1.9  begin
    1.10  
    1.11    (* Why should I import Main just to solve the Typerep problem! *)