| Thu, 07 Dec 2023 11:51:03 +0100 |
wenzelm |
clarified signature: more standard argument order;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Fri, 10 Jun 2016 15:53:08 +0100 |
paulson |
code to catch exception TERM in blast
|
file |
diff |
annotate
|
| Fri, 10 Jun 2016 13:54:50 +0100 |
paulson |
Better treatment of assumptions/goals that are simply Boolean variables. Also cosmetic changes.
|
file |
diff |
annotate
|
| Mon, 12 Oct 2015 20:25:50 +0200 |
wenzelm |
proper message;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| Sun, 30 Aug 2015 20:57:34 +0200 |
wenzelm |
trim context for persistent storage;
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 11:46:08 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Mon, 10 Nov 2014 21:49:48 +0100 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
file |
diff |
annotate
|
| Sun, 09 Nov 2014 18:27:43 +0100 |
wenzelm |
proper context;
|
file |
diff |
annotate
|
| Sun, 09 Nov 2014 17:04:14 +0100 |
wenzelm |
proper context for match_tac etc.;
|
file |
diff |
annotate
|
| Sun, 09 Nov 2014 14:08:00 +0100 |
wenzelm |
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
|
file |
diff |
annotate
|
| Sat, 08 Nov 2014 21:31:51 +0100 |
wenzelm |
optional proof context for unify operations, for the sake of proper local options;
|
file |
diff |
annotate
|
| Thu, 30 Oct 2014 16:55:29 +0100 |
wenzelm |
eliminated aliases;
|
file |
diff |
annotate
|
| Wed, 29 Oct 2014 19:01:49 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Tue, 07 Jan 2014 23:55:51 +0100 |
wenzelm |
avoid hard tabs in output -- somewhat ill-defined;
|
file |
diff |
annotate
|
| Tue, 07 Jan 2014 23:44:33 +0100 |
wenzelm |
uniform output of tracing via official channel (usually depending on trace flag);
|
file |
diff |
annotate
|
| Wed, 01 Jan 2014 20:14:47 +0100 |
wenzelm |
clarified blast after change of SELECT_GOAL in 210bca64b894: do not smash flex-flex pairs of overall goal state (in analogy to maxidx) -- NB: Isar goal structure serves as natural boundary, e.g. in "by blast";
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Wed, 11 Sep 2013 14:23:06 +0200 |
wenzelm |
do not expose internal flags to attribute name space;
|
file |
diff |
annotate
|
| Mon, 27 Feb 2012 19:53:34 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 10 Jun 2011 13:32:51 +0200 |
wenzelm |
local gensym based on Name.variant;
|
file |
diff |
annotate
|
| Fri, 10 Jun 2011 12:51:29 +0200 |
wenzelm |
uniform use of flexflex_rule;
|
file |
diff |
annotate
|
| Fri, 10 Jun 2011 11:39:23 +0200 |
wenzelm |
more official options blast_trace, blast_stats;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 22:13:21 +0200 |
wenzelm |
clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
|
file |
diff |
annotate
|
| Mon, 30 May 2011 12:15:17 +0100 |
paulson |
Fix to exception THM 1 raised (line 212 of conv.ML), reported by Andreas Lochbihler
|
file |
diff |
annotate
|
| Sun, 15 May 2011 16:40:24 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 14 May 2011 16:12:42 +0200 |
wenzelm |
eliminated global Unsynchronized.ref;
|
file |
diff |
annotate
|
| Sat, 14 May 2011 13:32:33 +0200 |
wenzelm |
simplified BLAST_DATA;
|
file |
diff |
annotate
|
| Sat, 14 May 2011 13:26:55 +0200 |
wenzelm |
proper Proof.context -- eliminated global operations;
|
file |
diff |
annotate
|
| Fri, 13 May 2011 22:55:00 +0200 |
wenzelm |
proper Proof.context for classical tactics;
|
file |
diff |
annotate
|
| Mon, 02 May 2011 16:33:21 +0200 |
wenzelm |
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
|
file |
diff |
annotate
|
| Tue, 26 Apr 2011 21:27:01 +0200 |
wenzelm |
simplified Blast setup;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 21:45:47 +0200 |
wenzelm |
tuned blast: navigate to subgoal only once;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 20:26:59 +0200 |
wenzelm |
more direct Thm.cprem_of (with exception THM instead of Subscript);
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 18:11:20 +0200 |
wenzelm |
eliminated old List.nth;
|
file |
diff |
annotate
|
| Sun, 20 Mar 2011 21:28:11 +0100 |
wenzelm |
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
|
file |
diff |
annotate
|
| Mon, 10 Jan 2011 15:45:46 +0100 |
wenzelm |
eliminated Int.toString;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| Mon, 10 May 2010 20:53:06 +0200 |
wenzelm |
renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
|
file |
diff |
annotate
|
| Sun, 28 Mar 2010 16:59:06 +0200 |
wenzelm |
static defaults for configuration options;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
| Sat, 06 Mar 2010 15:39:16 +0100 |
wenzelm |
eliminated Args.bang_facts (legacy feature);
|
file |
diff |
annotate
|
| Sun, 01 Nov 2009 15:44:26 +0100 |
wenzelm |
modernized structure Context_Rules;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Fri, 24 Jul 2009 21:21:45 +0200 |
wenzelm |
renamed functor BlastFun to Blast, require explicit theory;
|
file |
diff |
annotate
|
| Fri, 24 Jul 2009 21:02:34 +0200 |
wenzelm |
explicit OldGoals;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 01:03:18 +0200 |
wenzelm |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 21:24:30 +0200 |
wenzelm |
structure Thm: less pervasive names;
|
file |
diff |
annotate
|
| Thu, 26 Mar 2009 14:14:02 +0100 |
wenzelm |
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
|
file |
diff |
annotate
|
| Fri, 20 Mar 2009 17:12:37 +0100 |
wenzelm |
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
|
file |
diff |
annotate
|
| Tue, 17 Mar 2009 14:09:20 +0100 |
wenzelm |
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
|
file |
diff |
annotate
|
| Sun, 15 Mar 2009 20:25:58 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 21:25:15 +0100 |
wenzelm |
eliminated type Args.T;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2009 22:50:30 +0100 |
wenzelm |
eliminated Output.immediate_output -- violates the official message channel protocol;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Sun, 01 Mar 2009 23:36:12 +0100 |
wenzelm |
use long names for old-style fold combinators;
|
file |
diff |
annotate
|