| changeset 17926 | 8e12d3a4b890 |
| parent 17057 | 0934ac31985f |
| child 18678 | dd0c569fa43d |
| 17925:80a528111a82 | 17926:8e12d3a4b890 |
|---|---|
105 |
105 |
106 val _ = OuterSyntax.add_parsers [constsP]; |
106 val _ = OuterSyntax.add_parsers [constsP]; |
107 |
107 |
108 end; |
108 end; |
109 |
109 |
110 |
|
111 (* old-style theory syntax *) |
|
112 |
|
113 val _ = ThySyn.add_syntax [] |
|
114 [ThyParse.section "consts" "|> ContConsts.add_consts" ThyParse.const_decls]; |
|
115 |
|
116 end; |
110 end; |