changeset 30989 | 1f39aea228b0 |
parent 30988 | b53800e3ee47 |
child 31775 | 2b04504fcb69 |
--- a/src/HOL/Wellfounded.thy Sun Apr 26 08:34:53 2009 +0200 +++ b/src/HOL/Wellfounded.thy Sun Apr 26 20:23:09 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