| changeset 22140 | 0d49078c28bd |
| parent 22067 | 39d5d42116c4 |
| child 22167 | c3afded569ea |
--- a/src/HOL/ex/ROOT.ML Sat Jan 20 14:09:27 2007 +0100 +++ b/src/HOL/ex/ROOT.ML Sat Jan 20 14:27:45 2007 +0100 @@ -17,6 +17,7 @@ time_use_thy "Higher_Order_Logic"; time_use_thy "Abstract_NAT"; time_use_thy "Guess"; +time_use_thy "Binary"; time_use_thy "Recdefs"; time_use_thy "InductiveInvariant_examples";