changeset 58893 | 9e0ecb66d6a7 |
parent 58892 | 20aa19ecf2cc |
child 58923 | cb9b69cca999 |
--- a/src/Tools/try.ML Mon Nov 03 14:31:15 2014 +0100 +++ b/src/Tools/try.ML Mon Nov 03 14:50:27 2014 +0100 @@ -75,7 +75,7 @@ |> tap (fn NONE => writeln "Tried in vain." | _ => ()) val _ = - Outer_Syntax.improper_command @{command_spec "try"} + Outer_Syntax.command @{command_spec "try"} "try a combination of automatic proving and disproving tools" (Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))