equal
deleted
inserted
replaced
14 val someN: string |
14 val someN: string |
15 val noneN: string |
15 val noneN: string |
16 val unknownN: string |
16 val unknownN: string |
17 val max_solutions: int Unsynchronized.ref |
17 val max_solutions: int Unsynchronized.ref |
18 val solve_direct: Proof.state -> bool * (string * Proof.state) |
18 val solve_direct: Proof.state -> bool * (string * Proof.state) |
19 val setup: theory -> theory |
|
20 end; |
19 end; |
21 |
20 |
22 structure Solve_Direct: SOLVE_DIRECT = |
21 structure Solve_Direct: SOLVE_DIRECT = |
23 struct |
22 struct |
24 |
23 |
113 |
112 |
114 (* hook *) |
113 (* hook *) |
115 |
114 |
116 fun try_solve_direct auto = do_solve_direct (if auto then Auto_Try else Try) |
115 fun try_solve_direct auto = do_solve_direct (if auto then Auto_Try else Try) |
117 |
116 |
118 val setup = Try.register_tool (solve_directN, (10, @{option auto_solve_direct}, try_solve_direct)); |
117 val _ = Try.tool_setup (solve_directN, (10, @{option auto_solve_direct}, try_solve_direct)); |
119 |
118 |
120 end; |
119 end; |