src/HOL/Relation_Power.thy
changeset 26072 f65a7fa2da6c
parent 25861 494d9301cc75
child 26799 5bd38256ce5b
--- a/src/HOL/Relation_Power.thy	Fri Feb 15 16:09:10 2008 +0100
+++ b/src/HOL/Relation_Power.thy	Fri Feb 15 16:09:12 2008 +0100
@@ -7,7 +7,7 @@
 header{*Powers of Relations and Functions*}
 
 theory Relation_Power
-imports Power
+imports Power Transitive_Closure
 begin
 
 instance