src/HOL/ROOT.ML
changeset 7548 9e29a3af64ab
parent 7370 6407a09ac58f
child 7703 6b3424e877bd
     1.1 --- a/src/HOL/ROOT.ML	Tue Sep 21 11:11:09 1999 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Tue Sep 21 14:13:45 1999 +0200
     1.3 @@ -56,7 +56,6 @@
     1.4  use_thy "IntDef";
     1.5  use "simproc.ML";
     1.6  use_thy "NatBin";
     1.7 -use "bin_simprocs.ML";
     1.8  cd "..";
     1.9  
    1.10  (*the all-in-one theory*)