src/HOL/ROOT.ML
changeset 5560 c17471a9c99c
parent 5501 a63e0c326e6c
child 5606 39d68cfa457d
     1.1 --- a/src/HOL/ROOT.ML	Fri Sep 25 12:03:11 1998 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Fri Sep 25 12:12:07 1998 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4  use "Tools/datatype_abs_proofs.ML";
     1.5  use "Tools/datatype_package.ML";
     1.6  use "Tools/primrec_package.ML";
     1.7 -use_thy"Datatype";
     1.8 +use_thy "Datatype";
     1.9  
    1.10  use_thy "Arith";
    1.11  use "arith_data.ML";
    1.12 @@ -65,7 +65,7 @@
    1.13  
    1.14  cd "Integ";
    1.15  use_thy "IntDef";
    1.16 -use     "simproc";
    1.17 +use "simproc.ML";
    1.18  use_thy "Bin";
    1.19  cd "..";
    1.20