# HG changeset patch
# User blanchet
# Date 1292755722 -3600
# Node ID 8e1cde88aae6f3db7e8a17e02d3828301af1d90e
# Parent  1369c27c6966b2230df3fc1a4e6822fa96ec349d
added a timestamp to Nitpick in verbose mode for debugging purposes;
turn on verbose mode for the examples

diff -r 1369c27c6966 -r 8e1cde88aae6 src/HOL/Nitpick_Examples/Core_Nits.thy
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Sun Dec 19 00:13:25 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Sun Dec 19 11:48:42 2010 +0100
@@ -11,7 +11,7 @@
 imports Main
 begin
 
-nitpick_params [card = 1\<midarrow>6, unary_ints, max_potential = 0,
+nitpick_params [verbose, card = 1\<midarrow>6, unary_ints, max_potential = 0,
                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
 
 subsection {* Curry in a Hurry *}
diff -r 1369c27c6966 -r 8e1cde88aae6 src/HOL/Nitpick_Examples/Datatype_Nits.thy
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Sun Dec 19 00:13:25 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Sun Dec 19 11:48:42 2010 +0100
@@ -11,7 +11,7 @@
 imports Main
 begin
 
-nitpick_params [card = 1\<midarrow>8, max_potential = 0,
+nitpick_params [verbose, card = 1\<midarrow>8, max_potential = 0,
                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
 
 primrec rot where
diff -r 1369c27c6966 -r 8e1cde88aae6 src/HOL/Nitpick_Examples/Hotel_Nits.thy
--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Sun Dec 19 00:13:25 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy	Sun Dec 19 11:48:42 2010 +0100
@@ -12,8 +12,8 @@
 imports Main
 begin
 
-nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
-                timeout = 120]
+nitpick_params [verbose, max_potential = 0, sat_solver = MiniSat_JNI,
+                max_threads = 1, timeout = 120]
 
 typedecl guest
 typedecl key
diff -r 1369c27c6966 -r 8e1cde88aae6 src/HOL/Nitpick_Examples/Induct_Nits.thy
--- a/src/HOL/Nitpick_Examples/Induct_Nits.thy	Sun Dec 19 00:13:25 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy	Sun Dec 19 11:48:42 2010 +0100
@@ -11,8 +11,8 @@
 imports Main
 begin
 
-nitpick_params [card = 1\<midarrow>8, unary_ints, sat_solver = MiniSat_JNI,
-                max_threads = 1, timeout = 60]
+nitpick_params [verbose, card = 1\<midarrow>8, unary_ints,
+                sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
 
 inductive p1 :: "nat \<Rightarrow> bool" where
 "p1 0" |
diff -r 1369c27c6966 -r 8e1cde88aae6 src/HOL/Nitpick_Examples/Integer_Nits.thy
--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy	Sun Dec 19 00:13:25 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy	Sun Dec 19 11:48:42 2010 +0100
@@ -11,7 +11,7 @@
 imports Nitpick
 begin
 
-nitpick_params [card = 1\<midarrow>5, bits = 1,2,3,4,6,
+nitpick_params [verbose, card = 1\<midarrow>5, bits = 1,2,3,4,6,
                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
 
 lemma "Suc x = x + 1"
diff -r 1369c27c6966 -r 8e1cde88aae6 src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Sun Dec 19 00:13:25 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Sun Dec 19 11:48:42 2010 +0100
@@ -17,7 +17,8 @@
 
 chapter {* 3. First Steps *}
 
-nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
+nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1,
+                timeout = 60]
 
 subsection {* 3.1. Propositional Logic *}
 
diff -r 1369c27c6966 -r 8e1cde88aae6 src/HOL/Nitpick_Examples/Pattern_Nits.thy
--- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Sun Dec 19 00:13:25 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Sun Dec 19 11:48:42 2010 +0100
@@ -11,7 +11,7 @@
 imports Main
 begin
 
-nitpick_params [card = 10, max_potential = 0, sat_solver = MiniSat_JNI,
+nitpick_params [verbose, card = 10, max_potential = 0, sat_solver = MiniSat_JNI,
                 max_threads = 1, timeout = 60]
 
 lemma "x = (case u of () \<Rightarrow> y)"
diff -r 1369c27c6966 -r 8e1cde88aae6 src/HOL/Nitpick_Examples/Record_Nits.thy
--- a/src/HOL/Nitpick_Examples/Record_Nits.thy	Sun Dec 19 00:13:25 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Record_Nits.thy	Sun Dec 19 11:48:42 2010 +0100
@@ -11,7 +11,7 @@
 imports Main
 begin
 
-nitpick_params [card = 1\<midarrow>6, max_potential = 0,
+nitpick_params [verbose, card = 1\<midarrow>6, max_potential = 0,
                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
 
 record point2d =
diff -r 1369c27c6966 -r 8e1cde88aae6 src/HOL/Nitpick_Examples/Refute_Nits.thy
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Sun Dec 19 00:13:25 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Sun Dec 19 11:48:42 2010 +0100
@@ -11,7 +11,7 @@
 imports Main
 begin
 
-nitpick_params [card = 1\<midarrow>6, max_potential = 0,
+nitpick_params [verbose, card = 1\<midarrow>6, max_potential = 0,
                 sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
 
 lemma "P \<and> Q"
diff -r 1369c27c6966 -r 8e1cde88aae6 src/HOL/Nitpick_Examples/Special_Nits.thy
--- a/src/HOL/Nitpick_Examples/Special_Nits.thy	Sun Dec 19 00:13:25 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Special_Nits.thy	Sun Dec 19 11:48:42 2010 +0100
@@ -11,7 +11,7 @@
 imports Main
 begin
 
-nitpick_params [card = 4, sat_solver = MiniSat_JNI, max_threads = 1,
+nitpick_params [verbose, card = 4, sat_solver = MiniSat_JNI, max_threads = 1,
                 timeout = 60]
 
 fun f1 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
diff -r 1369c27c6966 -r 8e1cde88aae6 src/HOL/Nitpick_Examples/Typedef_Nits.thy
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Sun Dec 19 00:13:25 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Sun Dec 19 11:48:42 2010 +0100
@@ -11,7 +11,7 @@
 imports Complex_Main
 begin
 
-nitpick_params [card = 1\<midarrow>4, sat_solver = MiniSat_JNI, max_threads = 1,
+nitpick_params [verbose, card = 1\<midarrow>4, sat_solver = MiniSat_JNI, max_threads = 1,
                 timeout = 60]
 
 typedef three = "{0\<Colon>nat, 1, 2}"
diff -r 1369c27c6966 -r 8e1cde88aae6 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Sun Dec 19 00:13:25 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sun Dec 19 11:48:42 2010 +0100
@@ -246,6 +246,8 @@
                    "subgoal " ^ string_of_int i ^ " of " ^ string_of_int n
                  else
                    "goal")) [Logic.list_implies (assm_ts, orig_t)]))
+    val _ = print_v (enclose "Timestamp: " "." o Date.fmt "%H:%M:%S"
+                     o Date.fromTimeLocal o Time.now)
     val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
                 else orig_t
     val tfree_table =