| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Tue, 06 Jun 2017 13:13:25 +0200 |
wenzelm |
discontinued obsolete print mode;
|
file |
diff |
annotate
|
| Tue, 29 Mar 2016 21:17:29 +0200 |
wenzelm |
more position information for type mixfix;
|
file |
diff |
annotate
|
| Wed, 07 Oct 2015 15:31:59 +0200 |
blanchet |
avoid 'legacy binding' warning
|
file |
diff |
annotate
|
| Wed, 07 Oct 2015 15:31:47 +0200 |
blanchet |
removed dead code
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 11:50:23 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 09:27:31 +0200 |
blanchet |
avoid legacy syntax
|
file |
diff |
annotate
|
| Mon, 05 Oct 2015 15:57:25 +0200 |
blanchet |
avoid unsound simplification of (C (s x)) when s is a selector but not C's
|
file |
diff |
annotate
|
| Thu, 13 Aug 2015 11:05:19 +0200 |
wenzelm |
tuned signature, in accordance to sortBy in Scala;
|
file |
diff |
annotate
|
| Fri, 29 May 2015 17:56:43 +0200 |
blanchet |
removed model checks from Nitpick
|
file |
diff |
annotate
|
| Wed, 22 Apr 2015 23:26:14 +0200 |
blanchet |
avoid binding warning in Nitpick
|
file |
diff |
annotate
|
| Mon, 20 Apr 2015 11:23:00 +0200 |
blanchet |
declare Nitpick atoms to avoid '??.' prefixes in output
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 19:39:08 +0200 |
wenzelm |
proper context for Object_Logic operations;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 11:36:41 +0100 |
wenzelm |
discontinued obsolete Output.urgent_message;
|
file |
diff |
annotate
|
| Wed, 08 Oct 2014 17:09:07 +0200 |
wenzelm |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 18:19:57 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Wed, 19 Mar 2014 22:10:33 +0100 |
wenzelm |
more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 22:33:22 +0100 |
blanchet |
tuned ML names
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 22:33:22 +0100 |
blanchet |
tuned code
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 22:33:22 +0100 |
blanchet |
removed nonstandard models from Nitpick
|
file |
diff |
annotate
|
| Mon, 24 Feb 2014 14:58:40 +0100 |
wenzelm |
prefer standard Proof_Context.transfer, with theory stamp transfer (should now work thanks to purely functional theory, without Theory.copy etc.);
|
file |
diff |
annotate
|
| Thu, 19 Dec 2013 13:43:21 +0100 |
blanchet |
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file |
diff |
annotate
|
| Thu, 18 Jul 2013 13:12:54 +0200 |
wenzelm |
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 -> 100000, JinjaThreads: 65000 -> 300000) -- minimal measurable impact on inference kernel performance;
|
file |
diff |
annotate
|
| Mon, 27 May 2013 15:14:41 +0200 |
blanchet |
get rid of "show_all_types" in Nitpick
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
optimized MaSh output by chunking it
|
file |
diff |
annotate
|
| Fri, 11 May 2012 00:45:24 +0200 |
blanchet |
fixed "real" after they were redefined as a 'quotient_type'
|
file |
diff |
annotate
|
| Wed, 04 Jan 2012 12:09:53 +0100 |
blanchet |
handle higher-order occurrences of sets gracefully in model display
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 18:33:18 +0100 |
blanchet |
no abuse of notation
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 18:33:18 +0100 |
blanchet |
create consts with proper "set" types
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 18:33:17 +0100 |
blanchet |
port part of Nitpick to "set" type constructor
|
file |
diff |
annotate
|
| Sun, 13 Nov 2011 20:28:22 +0100 |
blanchet |
avoid confusing selector output
|
file |
diff |
annotate
|
| Fri, 13 May 2011 22:55:00 +0200 |
wenzelm |
proper Proof.context for classical tactics;
|
file |
diff |
annotate
|
| Tue, 19 Apr 2011 14:04:58 +0200 |
blanchet |
use "Spec_Rules" for finding axioms -- more reliable and cleaner
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 19:54:04 +0200 |
wenzelm |
report Name_Space.declare/define, relatively to context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Thu, 17 Mar 2011 22:07:17 +0100 |
blanchet |
reintroduced "show_skolems" option -- useful when too many Skolems are displayed
|
file |
diff |
annotate
|
| Thu, 03 Mar 2011 11:20:48 +0100 |
blanchet |
renamed "preconstr" option "need"
|
file |
diff |
annotate
|
| Wed, 02 Mar 2011 14:50:16 +0100 |
blanchet |
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 17:36:32 +0100 |
blanchet |
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 10:42:29 +0100 |
blanchet |
always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"
|
file |
diff |
annotate
|
| Sat, 08 Jan 2011 17:14:48 +0100 |
wenzelm |
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 11:56:53 +0100 |
blanchet |
remove the "fin_fun" optimization in Nitpick -- it was always a hack and didn't help much
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 14:47:58 +0100 |
blanchet |
show strings as "s_1" etc. rather than "l_1" etc.
|
file |
diff |
annotate
|
| Sat, 20 Nov 2010 00:53:26 +0100 |
wenzelm |
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 21:06:56 +0200 |
wenzelm |
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
|
file |
diff |
annotate
|
| Tue, 14 Sep 2010 13:44:43 +0200 |
blanchet |
eliminate more clutter related to "fast_descrs" optimization
|
file |
diff |
annotate
|
| Tue, 14 Sep 2010 13:24:18 +0200 |
blanchet |
remove "fast_descs" option from Nitpick;
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 20:21:40 +0200 |
blanchet |
remove unreferenced identifiers
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 17:43:44 +0200 |
wenzelm |
turned show_all_types into proper configuration option;
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
| Mon, 09 Aug 2010 12:40:15 +0200 |
blanchet |
use "declaration" instead of "setup" to register Nitpick extensions
|
file |
diff |
annotate
|
| Fri, 06 Aug 2010 17:05:29 +0200 |
blanchet |
local versions of Nitpick.register_xxx functions
|
file |
diff |
annotate
|
| Thu, 05 Aug 2010 20:17:50 +0200 |
blanchet |
added "whack"
|
file |
diff |
annotate
|
| Thu, 05 Aug 2010 18:00:50 +0200 |
blanchet |
added support for "Abs_" and "Rep_" functions on quotient types
|
file |
diff |
annotate
|
| Wed, 04 Aug 2010 10:39:35 +0200 |
blanchet |
get rid of all "optimizations" regarding "unit" and other cardinality-1 types
|
file |
diff |
annotate
|
| Tue, 03 Aug 2010 21:37:12 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|