src/ZF/ROOT.ML
changeset 516 1957113f0d7d
parent 488 52f7447d4f1b
child 532 851df239ac8b
     1.1 --- a/src/ZF/ROOT.ML	Fri Aug 12 12:28:46 1994 +0200
     1.2 +++ b/src/ZF/ROOT.ML	Fri Aug 12 12:51:34 1994 +0200
     1.3 @@ -28,8 +28,20 @@
     1.4  
     1.5  print_depth 1;
     1.6  
     1.7 +(*Add user sections for inductive/datatype definitions*)
     1.8 +use_thy "Datatype";
     1.9 +structure ThySyn = ThySynFun
    1.10 + (val user_keywords = ["inductive", "coinductive", "datatype", "codatatype", 
    1.11 +		       "and", "|", "<=", "domains", "intrs", "monos", 
    1.12 +		       "con_defs", "type_intrs", "type_elims"] 
    1.13 +  and user_sections = [("inductive",  inductive_decl ""),
    1.14 +		       ("coinductive",  inductive_decl "Co"),
    1.15 +		       ("datatype",  datatype_decl ""),
    1.16 +		       ("codatatype",  datatype_decl "Co")]);
    1.17 +init_thy_reader ();
    1.18 +
    1.19  use_thy "InfDatatype";
    1.20 -use_thy "ListFn";
    1.21 +use_thy "List";
    1.22  
    1.23  (*printing functions are inherited from FOL*)
    1.24  print_depth 8;