Lines Matching defs:proof
5 datatype proof
9 datatype proofs = PRFS of proof list
12 (* Starting a proof *)
13 val new_goalstack : goal -> (thm->thm) -> proof
14 val new_goaltree : goal -> proof
15 val set_goal : goal -> proof
16 val add : proof -> proofs -> proofs
19 val backup : proof -> proof
20 val set_backup : int -> proof -> proof
21 val restore : proof -> proof
22 val save : proof -> proof
23 val forget_history : proof -> proof
24 val restart : proof -> proof
28 val expand : tactic -> proof -> proof
29 val expandf : tactic -> proof -> proof
30 val expand_list : list_tactic -> proof -> proof
31 val expand_listf : list_tactic -> proof -> proof
32 val expandv : string * tactic -> proof -> proof
34 (* Seeing what the state of the proof manager is *)
35 val top_thm : proof -> thm
36 val initial_goal : proof -> goal
37 val finalizer : proof -> (thm -> thm)
38 val top_goal : proof -> goal
39 val top_goals : proof -> goal list
40 val current_proof : proofs -> proof
42 (* Switch focus to a different subgoal (or proof attempt) *)
43 val rotate : int -> proof -> proof
44 val flatn : int -> proof -> proof
47 (* Operations on proof attempts *)
48 val hd_opr : (proof -> proof) -> proofs -> proofs
49 val hd_proj : (proof -> 'a) -> proofs -> 'a
55 val pp_proof : proof Parse.pprinter