src/HOL/ROOT.ML
changeset 2115 9709f9188549
parent 2019 b45d9f2042e0
child 2857 848bce5fe8ad
     1.1 --- a/src/HOL/ROOT.ML	Mon Oct 21 09:49:41 1996 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Mon Oct 21 09:50:50 1996 +0200
     1.3 @@ -19,6 +19,7 @@
     1.4  use "../Provers/splitter.ML";
     1.5  use "../Provers/hypsubst.ML";
     1.6  use "../Provers/classical.ML";
     1.7 +use "../Provers/nat_transitive.ML";
     1.8  
     1.9  
    1.10  use_thy "HOL";