equal
deleted
inserted
replaced
15 include BASIC_PRESENT |
15 include BASIC_PRESENT |
16 val init: bool -> string -> string list -> string -> Url.T option * bool -> unit |
16 val init: bool -> string -> string list -> string -> Url.T option * bool -> unit |
17 val finish: unit -> unit |
17 val finish: unit -> unit |
18 val init_theory: string -> unit |
18 val init_theory: string -> unit |
19 val verbatim_source: string -> (unit -> string list) -> unit |
19 val verbatim_source: string -> (unit -> string list) -> unit |
20 val token_source: string -> (unit -> OuterLex.token list) -> unit |
20 val token_source: string -> (unit -> (OuterLex.token * string option) list) -> unit |
21 val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory |
21 val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory |
22 val result: string -> string -> thm -> unit |
22 val result: string -> string -> thm -> unit |
23 val results: string -> string -> thm list -> unit |
23 val results: string -> string -> thm list -> unit |
24 val theorem: string -> thm -> unit |
24 val theorem: string -> thm -> unit |
25 val theorems: string -> thm list -> unit |
25 val theorems: string -> thm list -> unit |