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