blob: 2473af0c5ba6fbd62e99c35032c5471e42f80a2c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
(* $Id$ *)
(*i*)
open Pp
open Sign
open Declare
open Proof_trees
open Refiner
(*i*)
val proof_prompt : unit -> string
val refining : unit -> bool
val msg_proofs : bool -> std_ppcmds
val undo_limit : int ref
val set_undo : int -> unit
val unset_undo : unit -> unit
type proof_topstate = {
top_hyps : context * context;
top_goal : goal;
top_strength : strength }
val get_state : unit -> pftreestate * proof_topstate
val get_topstate : unit -> proof_topstate
val get_pftreestate : unit -> pftreestate
val get_evmap_sign : int option -> evar_declarations * context
val set_proof : string option -> unit
val get_proof : unit -> string
val list_proofs : unit -> string list
val add_proof : string * pftreestate * proof_topstate -> unit
val del_proof : string -> unit
val init_proofs : unit -> unit
|
