src/HOL/Tools/Nitpick/nitpick_commands.ML
changeset 59936 b8ffc3dc9e24
parent 59058 a78612c67ec0
child 60094 96a4765ba7d1
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Mon Apr 06 16:30:44 2015 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Mon Apr 06 17:06:48 2015 +0200
     1.3 @@ -374,7 +374,7 @@
     1.4                                        |> sort_strings |> cat_lines)))))
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.command @{command_spec "nitpick"}
     1.8 +  Outer_Syntax.command @{command_keyword nitpick}
     1.9      "try to find a counterexample for a given subgoal using Nitpick"
    1.10      (parse_params -- Scan.optional Parse.nat 1 >> (fn (params, i) =>
    1.11        Toplevel.unknown_proof o
    1.12 @@ -383,7 +383,7 @@
    1.13            (Toplevel.proof_of state)))))
    1.14  
    1.15  val _ =
    1.16 -  Outer_Syntax.command @{command_spec "nitpick_params"}
    1.17 +  Outer_Syntax.command @{command_keyword nitpick_params}
    1.18      "set and display the default parameters for Nitpick"
    1.19      (parse_params #>> nitpick_params_trans)
    1.20