equal
deleted
inserted
replaced
28 structure HOL4ImportSyntax :> HOL4_IMPORT_SYNTAX = |
28 structure HOL4ImportSyntax :> HOL4_IMPORT_SYNTAX = |
29 struct |
29 struct |
30 |
30 |
31 type token = OuterSyntax.token |
31 type token = OuterSyntax.token |
32 |
32 |
33 local structure P = OuterParse and K = OuterSyntax.Keyword in |
33 local structure P = OuterParse and K = OuterKeyword in |
34 |
34 |
35 (* Parsers *) |
35 (* Parsers *) |
36 |
36 |
37 val import_segment = P.name >> set_import_segment |
37 val import_segment = P.name >> set_import_segment |
38 |
38 |