src/HOL/Wellfounded.thy
changeset 30988 b53800e3ee47
parent 30430 42ea5d85edcc
child 30989 1f39aea228b0
     1.1 --- a/src/HOL/Wellfounded.thy	Sun Apr 26 00:42:59 2009 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Sun Apr 26 08:34:53 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 Transitive_Closure Nat
     1.8 +imports Finite_Set Wellfounded Nat
     1.9  uses ("Tools/function_package/size.ML")
    1.10  begin
    1.11