# HG changeset patch
# User haftmann
# Date 1240770221 -7200
# Node ID a1efb13fc5d8b8cf356676a7d9cdd60eacb3224f
# Parent  b057748ccebe42c5eeb2ffc9520859dccee44c9b# Parent  1f39aea228b00fbeb5041c34f657d878c54fe518
merged

diff -r b057748ccebe -r a1efb13fc5d8 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Sun Apr 26 20:18:48 2009 +0200
+++ b/src/HOL/Wellfounded.thy	Sun Apr 26 20:23:41 2009 +0200
@@ -7,7 +7,7 @@
 header {*Well-founded Recursion*}
 
 theory Wellfounded
-imports Finite_Set Wellfounded Nat
+imports Finite_Set Transitive_Closure
 uses ("Tools/function_package/size.ML")
 begin