disable auto_nitpick for now: spurious problems with non-termination e.g. in HOL-Hoare examples;
authorwenzelm
Wed, 23 Dec 2020 21:15:21 +0100
changeset 72988 52ba78df4088
parent 72987 b1be35908165
child 72989 5906162c8dd4
disable auto_nitpick for now: spurious problems with non-termination e.g. in HOL-Hoare examples;
src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options	Wed Dec 23 21:06:31 2020 +0100
+++ b/src/HOL/Tools/etc/options	Wed Dec 23 21:15:21 2020 +0100
@@ -8,7 +8,7 @@
 public option auto_time_limit : real = 2.0
   -- "time limit for automatically tried tools (seconds > 0)"
 
-public option auto_nitpick : bool = true
+public option auto_nitpick : bool = false
   -- "run Nitpick automatically"
 
 public option auto_sledgehammer : bool = false