explicitly import Fact
authorhuffman
Mon Feb 23 10:42:31 2009 -0800 (2009-02-23)
changeset 3007438ce654e1b05
parent 30073 a4ad0c08b7d9
child 30075 ff5b4900d9a5
explicitly import Fact
src/HOL/Library/Permutations.thy
     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! *)