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