equal
deleted
inserted
replaced
17 val add_keywords: keywords -> theory -> theory |
17 val add_keywords: keywords -> theory -> theory |
18 val get_keywords: theory -> Keyword.keywords |
18 val get_keywords: theory -> Keyword.keywords |
19 val get_keywords': Proof.context -> Keyword.keywords |
19 val get_keywords': Proof.context -> Keyword.keywords |
20 val ml_bootstrapN: string |
20 val ml_bootstrapN: string |
21 val ml_roots: string list |
21 val ml_roots: string list |
|
22 val bootstrap_thys: string list |
22 val args: header parser |
23 val args: header parser |
23 val read: Position.T -> string -> header |
24 val read: Position.T -> string -> header |
24 val read_tokens: Token.T list -> header |
25 val read_tokens: Token.T list -> header |
25 end; |
26 end; |
26 |
27 |
106 |
107 |
107 (* names *) |
108 (* names *) |
108 |
109 |
109 val ml_bootstrapN = "ML_Bootstrap"; |
110 val ml_bootstrapN = "ML_Bootstrap"; |
110 val ml_roots = ["ML_Root0", "ML_Root"]; |
111 val ml_roots = ["ML_Root0", "ML_Root"]; |
|
112 val bootstrap_thys = ["Bootstrap_Pure", "Bootstrap_ML_Bootstrap"]; |
111 |
113 |
112 |
114 |
113 |
115 |
114 (* header args *) |
116 (* header args *) |
115 |
117 |