src/HOL/Tools/Nitpick/nitpick_isar.ML
changeset 43865 58150aa44941
parent 43863 7d3ce43d9464
child 43873 f617a5323d07
equal deleted inserted replaced
43864:cb8d4c2af639 43865:58150aa44941
   401             "set and display the default parameters for Nitpick"
   401             "set and display the default parameters for Nitpick"
   402             Keyword.thy_decl parse_nitpick_params_command
   402             Keyword.thy_decl parse_nitpick_params_command
   403 
   403 
   404 fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0
   404 fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0
   405 
   405 
   406 val setup = Try.register_tool (nitpickN, (auto, try_nitpick))
   406 val setup = Try.register_tool (nitpickN, (50, auto, try_nitpick))
   407 
   407 
   408 end;
   408 end;