changeset 59936 | b8ffc3dc9e24 |
parent 59184 | 830bb7ddb3ab |
child 60094 | 96a4765ba7d1 |
--- a/src/Tools/solve_direct.ML Mon Apr 06 16:30:44 2015 +0200 +++ b/src/Tools/solve_direct.ML Mon Apr 06 17:06:48 2015 +0200 @@ -92,7 +92,7 @@ val solve_direct = do_solve_direct Normal val _ = - Outer_Syntax.command @{command_spec "solve_direct"} + Outer_Syntax.command @{command_keyword solve_direct} "try to solve conjectures directly with existing theorems" (Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));