equal
deleted
inserted
replaced
10 type header = |
10 type header = |
11 {name: string * Position.T, |
11 {name: string * Position.T, |
12 imports: (string * Position.T) list, |
12 imports: (string * Position.T) list, |
13 keywords: keywords} |
13 keywords: keywords} |
14 val make: string * Position.T -> (string * Position.T) list -> keywords -> header |
14 val make: string * Position.T -> (string * Position.T) list -> keywords -> header |
|
15 val theoryN: string |
15 val bootstrap_keywords: Keyword.keywords |
16 val bootstrap_keywords: Keyword.keywords |
16 val add_keywords: keywords -> theory -> theory |
17 val add_keywords: keywords -> theory -> theory |
17 val get_keywords: theory -> Keyword.keywords |
18 val get_keywords: theory -> Keyword.keywords |
18 val get_keywords': Proof.context -> Keyword.keywords |
19 val get_keywords': Proof.context -> Keyword.keywords |
19 val args: header parser |
20 val args: header parser |