equal
deleted
inserted
replaced
36 int -> Time.time -> parsed_proof |
36 int -> Time.time -> parsed_proof |
37 |
37 |
38 (*tactic*) |
38 (*tactic*) |
39 val smt2_tac: Proof.context -> thm list -> int -> tactic |
39 val smt2_tac: Proof.context -> thm list -> int -> tactic |
40 val smt2_tac': Proof.context -> thm list -> int -> tactic |
40 val smt2_tac': Proof.context -> thm list -> int -> tactic |
41 end |
41 end; |
42 |
42 |
43 structure SMT2_Solver: SMT2_SOLVER = |
43 structure SMT2_Solver: SMT2_SOLVER = |
44 struct |
44 struct |
45 |
|
46 |
45 |
47 (* interface to external solvers *) |
46 (* interface to external solvers *) |
48 |
47 |
49 local |
48 local |
50 |
49 |
296 val smt2_tac = tac safe_solve |
295 val smt2_tac = tac safe_solve |
297 val smt2_tac' = tac (SOME oo apply_solver_and_replay) |
296 val smt2_tac' = tac (SOME oo apply_solver_and_replay) |
298 |
297 |
299 end |
298 end |
300 |
299 |
301 end |
300 end; |