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