--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Sun Dec 19 18:55:21 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Sun Dec 19 19:03:49 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 *}
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Sun Dec 19 18:55:21 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Sun Dec 19 19:03:49 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
--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy Sun Dec 19 18:55:21 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy Sun Dec 19 19:03:49 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
--- a/src/HOL/Nitpick_Examples/Induct_Nits.thy Sun Dec 19 18:55:21 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy Sun Dec 19 19:03:49 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" |
--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy Sun Dec 19 18:55:21 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Sun Dec 19 19:03:49 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"
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Sun Dec 19 18:55:21 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Sun Dec 19 19:03:49 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 *}
--- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy Sun Dec 19 18:55:21 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy Sun Dec 19 19:03:49 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)"
--- a/src/HOL/Nitpick_Examples/Record_Nits.thy Sun Dec 19 18:55:21 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Record_Nits.thy Sun Dec 19 19:03:49 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 =
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Sun Dec 19 18:55:21 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Sun Dec 19 19:03:49 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"
--- a/src/HOL/Nitpick_Examples/Special_Nits.thy Sun Dec 19 18:55:21 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Sun Dec 19 19:03:49 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
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Sun Dec 19 18:55:21 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Sun Dec 19 19:03:49 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}"
--- a/src/HOL/Tools/Nitpick/nitpick.ML Sun Dec 19 18:55:21 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Sun Dec 19 19:03:49 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 =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sun Dec 19 18:55:21 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sun Dec 19 19:03:49 2010 +0100
@@ -101,6 +101,8 @@
| explode_interval max (Facts.From i) = i upto i + max - 1
| explode_interval _ (Facts.Single i) = [i]
+val backquote =
+ raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`"
fun fact_from_ref ctxt reserved chained_ths (xthm as (xref, args)) =
let
val ths = Attrib.eval_thms ctxt [xthm]
@@ -109,7 +111,7 @@
^ "]") args)
fun nth_name j =
case xref of
- Facts.Fact s => "`" ^ s ^ "`" ^ bracket
+ Facts.Fact s => backquote s ^ bracket
| Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
| Facts.Named ((name, _), NONE) =>
make_name reserved (length ths > 1) (j + 1) name ^ bracket
@@ -804,8 +806,8 @@
else
let
val multi = length ths > 1
- val backquotify =
- enclose "`" "`" o string_for_term ctxt o close_form o prop_of
+ val backquote_thm =
+ backquote o string_for_term ctxt o close_form o prop_of
fun check_thms a =
case try (ProofContext.get_thms ctxt) a of
NONE => false
@@ -820,7 +822,7 @@
else
(((fn () =>
if name0 = "" then
- th |> backquotify
+ th |> backquote_thm
else
let
val name1 = Facts.extern facts name0