Lines Matching refs:string
5 val new_exporter : string ->
6 (string -> (string * Thm.thm) list -> unit) ->
7 {dest : data -> (string * Thm.thm) list option,
8 export : string -> unit,
9 mk : string list -> data * (string * Thm.thm) list}
11 val new_storage_attribute : string -> unit
12 val store_attribute : {attribute: string, thm_name : string} -> unit
14 val current_data : string -> (string * Thm.thm) list
15 val theory_data : {settype : string, thy: string} ->
16 (string * Thm.thm) list
17 val all_data : string -> (string * (string * Thm.thm) list) list
18 val data_storefn : string -> (string -> unit) option
20 string -> (string -> (string * Thm.thm) list -> unit) option
22 val all_set_types : unit -> string list