src/HOL/Wellfounded.thy
changeset 30988 b53800e3ee47
parent 30430 42ea5d85edcc
child 30989 1f39aea228b0
--- a/src/HOL/Wellfounded.thy	Sun Apr 26 00:42:59 2009 +0200
+++ b/src/HOL/Wellfounded.thy	Sun Apr 26 08:34:53 2009 +0200
@@ -7,7 +7,7 @@
 header {*Well-founded Recursion*}
 
 theory Wellfounded
-imports Finite_Set Transitive_Closure Nat
+imports Finite_Set Wellfounded Nat
 uses ("Tools/function_package/size.ML")
 begin