(* GUI refresh functions *)
val refresh_proof : unit -> unit
val refresh_goals : unit -> unit
(* GUI refresh functions *)
val refresh_proof : unit -> unit
val refresh_goals : unit -> unit
val decompose_uris_choice_callback :
(UriManager.uri * int * 'a) list ->
(UriManager.uri * int * 'b list) list
val decompose_uris_choice_callback :
(UriManager.uri * int * 'a) list ->
(UriManager.uri * int * 'b list) list
val whd_in_scratch : unit -> unit
val reduce_in_scratch : unit -> unit
val simpl_in_scratch : unit -> unit
val whd_in_scratch : unit -> unit
val reduce_in_scratch : unit -> unit
val simpl_in_scratch : unit -> unit