author | haftmann |
Sun, 26 Apr 2009 20:23:09 +0200 | |
changeset 30989 | 1f39aea228b0 |
parent 30988 | b53800e3ee47 |
child 30990 | 4872eef36167 |
child 30994 | ba5bce0c26de |
child 30999 | a1efb13fc5d8 |
--- 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