equal
deleted
inserted
replaced
36 |
36 |
37 val string_of_proof_method : proof_method -> string |
37 val string_of_proof_method : proof_method -> string |
38 val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic |
38 val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic |
39 val string_of_play_outcome : play_outcome -> string |
39 val string_of_play_outcome : play_outcome -> string |
40 val play_outcome_ord : play_outcome * play_outcome -> order |
40 val play_outcome_ord : play_outcome * play_outcome -> order |
41 |
|
42 val one_line_proof_text : int -> one_line_params -> string |
41 val one_line_proof_text : int -> one_line_params -> string |
43 val silence_proof_methods : bool -> Proof.context -> Proof.context |
42 val silence_proof_methods : bool -> Proof.context -> Proof.context |
44 end; |
43 end; |
45 |
44 |
46 structure Sledgehammer_Reconstructor : SLEDGEHAMMER_RECONSTRUCTOR = |
45 structure Sledgehammer_Reconstructor : SLEDGEHAMMER_RECONSTRUCTOR = |