# HG changeset patch
# User huffman
# Date 1235414551 28800
# Node ID 38ce654e1b05021426cafcfa7d6360259ae78bc0
# Parent  a4ad0c08b7d90deea69e35ad122f4f81d31294bb
explicitly import Fact

diff -r a4ad0c08b7d9 -r 38ce654e1b05 src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Mon Feb 23 07:58:13 2009 -0800
+++ b/src/HOL/Library/Permutations.thy	Mon Feb 23 10:42:31 2009 -0800
@@ -6,7 +6,7 @@
 header {* Permutations, both general and specifically on finite sets.*}
 
 theory Permutations
-imports Main Finite_Cartesian_Product Parity 
+imports Main Finite_Cartesian_Product Parity Fact
 begin
 
   (* Why should I import Main just to solve the Typerep problem! *)