# HG changeset patch # User boehmes # Date 1292781829 -3600 # Node ID f9dd7a95158f67c48349d5beb0a9a32520a9286e # Parent a4d1b5eef12e144d8509c67426ff505b287e5111# Parent e0400b05a62c947cc4422f4c970cb7d53c6a74a8 merged diff -r a4d1b5eef12e -r f9dd7a95158f src/HOL/Nitpick_Examples/Core_Nits.thy --- 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\6, unary_ints, max_potential = 0, +nitpick_params [verbose, card = 1\6, unary_ints, max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60] subsection {* Curry in a Hurry *} diff -r a4d1b5eef12e -r f9dd7a95158f src/HOL/Nitpick_Examples/Datatype_Nits.thy --- 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\8, max_potential = 0, +nitpick_params [verbose, card = 1\8, max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60] primrec rot where diff -r a4d1b5eef12e -r f9dd7a95158f src/HOL/Nitpick_Examples/Hotel_Nits.thy --- 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 diff -r a4d1b5eef12e -r f9dd7a95158f src/HOL/Nitpick_Examples/Induct_Nits.thy --- 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\8, unary_ints, sat_solver = MiniSat_JNI, - max_threads = 1, timeout = 60] +nitpick_params [verbose, card = 1\8, unary_ints, + sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60] inductive p1 :: "nat \ bool" where "p1 0" | diff -r a4d1b5eef12e -r f9dd7a95158f src/HOL/Nitpick_Examples/Integer_Nits.thy --- 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\5, bits = 1,2,3,4,6, +nitpick_params [verbose, card = 1\5, bits = 1,2,3,4,6, sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60] lemma "Suc x = x + 1" diff -r a4d1b5eef12e -r f9dd7a95158f src/HOL/Nitpick_Examples/Manual_Nits.thy --- 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 *} diff -r a4d1b5eef12e -r f9dd7a95158f src/HOL/Nitpick_Examples/Pattern_Nits.thy --- 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 () \ y)" diff -r a4d1b5eef12e -r f9dd7a95158f src/HOL/Nitpick_Examples/Record_Nits.thy --- 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\6, max_potential = 0, +nitpick_params [verbose, card = 1\6, max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60] record point2d = diff -r a4d1b5eef12e -r f9dd7a95158f src/HOL/Nitpick_Examples/Refute_Nits.thy --- 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\6, max_potential = 0, +nitpick_params [verbose, card = 1\6, max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60] lemma "P \ Q" diff -r a4d1b5eef12e -r f9dd7a95158f src/HOL/Nitpick_Examples/Special_Nits.thy --- 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 \ nat \ nat \ nat \ nat \ nat" where diff -r a4d1b5eef12e -r f9dd7a95158f src/HOL/Nitpick_Examples/Typedef_Nits.thy --- 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\4, sat_solver = MiniSat_JNI, max_threads = 1, +nitpick_params [verbose, card = 1\4, sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60] typedef three = "{0\nat, 1, 2}" diff -r a4d1b5eef12e -r f9dd7a95158f src/HOL/Tools/Nitpick/nitpick.ML --- 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 = diff -r a4d1b5eef12e -r f9dd7a95158f src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- 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