equal
deleted
inserted
replaced
30 |
30 |
31 (*Add user sections for inductive/datatype definitions*) |
31 (*Add user sections for inductive/datatype definitions*) |
32 use "../Pure/section_utils.ML"; |
32 use "../Pure/section_utils.ML"; |
33 use "thy_syntax.ML"; |
33 use "thy_syntax.ML"; |
34 |
34 |
|
35 use_thy "Let"; |
35 use_thy "InfDatatype"; |
36 use_thy "InfDatatype"; |
36 use_thy "List"; |
37 use_thy "List"; |
37 use_thy "EquivClass"; |
38 use_thy "EquivClass"; |
38 |
39 |
39 (*printing functions are inherited from FOL*) |
40 (*printing functions are inherited from FOL*) |