src/ZF/ROOT.ML
changeset 578 efc648d29dd0
parent 532 851df239ac8b
child 803 4c8333ab3eae
     1.1 --- a/src/ZF/ROOT.ML	Thu Aug 25 10:41:17 1994 +0200
     1.2 +++ b/src/ZF/ROOT.ML	Thu Aug 25 12:09:21 1994 +0200
     1.3 @@ -29,6 +29,7 @@
     1.4  print_depth 1;
     1.5  
     1.6  (*Add user sections for inductive/datatype definitions*)
     1.7 +use     "../Pure/section_utils.ML";
     1.8  use_thy "Datatype";
     1.9  structure ThySyn = ThySynFun
    1.10   (val user_keywords = ["inductive", "coinductive", "datatype", "codatatype",