src/HOL/Wellfounded.thy
changeset 30989 1f39aea228b0
parent 30988 b53800e3ee47
child 31775 2b04504fcb69
     1.1 --- a/src/HOL/Wellfounded.thy	Sun Apr 26 08:34:53 2009 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Sun Apr 26 20:23:09 2009 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  header {*Well-founded Recursion*}
     1.5  
     1.6  theory Wellfounded
     1.7 -imports Finite_Set Wellfounded Nat
     1.8 +imports Finite_Set Transitive_Closure
     1.9  uses ("Tools/function_package/size.ML")
    1.10  begin
    1.11