src/HOL/ex/ROOT.ML
changeset 19085 a1a251b297dd
parent 19022 0e6ec4fd204c
child 19148 f03a9a1cbe0e
     1.1 --- a/src/HOL/ex/ROOT.ML	Thu Feb 16 19:39:02 2006 +0100
     1.2 +++ b/src/HOL/ex/ROOT.ML	Thu Feb 16 21:11:58 2006 +0100
     1.3 @@ -5,6 +5,7 @@
     1.4  *)
     1.5  
     1.6  time_use_thy "Higher_Order_Logic";
     1.7 +time_use_thy "Abstract_NAT";
     1.8  
     1.9  time_use_thy "Recdefs";
    1.10  time_use_thy "InductiveInvariant_examples";