src/HOL/Wellfounded.thy
changeset 29609 a010aab5bed0
parent 29580 117b88da143c
child 30430 42ea5d85edcc
--- a/src/HOL/Wellfounded.thy	Wed Jan 21 23:40:23 2009 +0100
+++ b/src/HOL/Wellfounded.thy	Wed Jan 21 23:40:23 2009 +0100
@@ -7,7 +7,7 @@
 header {*Well-founded Recursion*}
 
 theory Wellfounded
-imports Finite_Set Nat
+imports Finite_Set Transitive_Closure Nat
 uses ("Tools/function_package/size.ML")
 begin