Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
explicitly import Fact
authorhuffman
Mon, 23 Feb 2009 10:42:31 -0800
changeset 30074 38ce654e1b05
parent 30073 a4ad0c08b7d9
child 30075 ff5b4900d9a5
explicitly import Fact
src/HOL/Library/Permutations.thy file | annotate | diff | comparison | revisions 
--- 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! *)
isabelle