equal
deleted
inserted
replaced
92 val solve_direct = do_solve_direct Normal |
92 val solve_direct = do_solve_direct Normal |
93 |
93 |
94 val _ = |
94 val _ = |
95 Outer_Syntax.command @{command_keyword solve_direct} |
95 Outer_Syntax.command @{command_keyword solve_direct} |
96 "try to solve conjectures directly with existing theorems" |
96 "try to solve conjectures directly with existing theorems" |
97 (Scan.succeed (Toplevel.keep (ignore o solve_direct o Toplevel.proof_of))); |
97 (Scan.succeed (Toplevel.keep_proof (ignore o solve_direct o Toplevel.proof_of))); |
98 |
98 |
99 |
99 |
100 (* hook *) |
100 (* hook *) |
101 |
101 |
102 fun try_solve_direct auto = do_solve_direct (if auto then Auto_Try else Try) |
102 fun try_solve_direct auto = do_solve_direct (if auto then Auto_Try else Try) |