src/HOL/ROOT.ML
changeset 4573 fe504f608835
parent 4517 fad9b7479dbe
child 4758 35f4ad4f055d
     1.1 --- a/src/HOL/ROOT.ML	Wed Jan 14 10:31:32 1998 +0100
     1.2 +++ b/src/HOL/ROOT.ML	Wed Jan 14 10:32:24 1998 +0100
     1.3 @@ -39,6 +39,8 @@
     1.4  use_thy "Sum";
     1.5  use_thy "Gfp";
     1.6  
     1.7 +use "record.ML";
     1.8 +
     1.9  use "datatype.ML";
    1.10  use_thy "Arith";
    1.11  use "arith_data.ML";