src/Provers/blast.ML
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Tue, 07 Jan 2014 23:55:51 +0100 wenzelm avoid hard tabs in output -- somewhat ill-defined;
Tue, 07 Jan 2014 23:44:33 +0100 wenzelm uniform output of tracing via official channel (usually depending on trace flag);
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";
Sat, 14 Dec 2013 17:28:05 +0100 wenzelm proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
Wed, 11 Sep 2013 14:23:06 +0200 wenzelm do not expose internal flags to attribute name space;
Mon, 27 Feb 2012 19:53:34 +0100 wenzelm tuned;
Fri, 10 Jun 2011 13:32:51 +0200 wenzelm local gensym based on Name.variant;
Fri, 10 Jun 2011 12:51:29 +0200 wenzelm uniform use of flexflex_rule;
Fri, 10 Jun 2011 11:39:23 +0200 wenzelm more official options blast_trace, blast_stats;
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);
Mon, 30 May 2011 12:15:17 +0100 paulson Fix to exception THM 1 raised (line 212 of conv.ML), reported by Andreas Lochbihler
Sun, 15 May 2011 16:40:24 +0200 wenzelm tuned signature;
Sat, 14 May 2011 16:12:42 +0200 wenzelm eliminated global Unsynchronized.ref;
Sat, 14 May 2011 13:32:33 +0200 wenzelm simplified BLAST_DATA;
Sat, 14 May 2011 13:26:55 +0200 wenzelm proper Proof.context -- eliminated global operations;
Fri, 13 May 2011 22:55:00 +0200 wenzelm proper Proof.context for classical tactics;
Mon, 02 May 2011 16:33:21 +0200 wenzelm added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
Tue, 26 Apr 2011 21:27:01 +0200 wenzelm simplified Blast setup;
Sat, 16 Apr 2011 21:45:47 +0200 wenzelm tuned blast: navigate to subgoal only once;
Sat, 16 Apr 2011 20:26:59 +0200 wenzelm more direct Thm.cprem_of (with exception THM instead of Subscript);
Sat, 16 Apr 2011 18:11:20 +0200 wenzelm eliminated old List.nth;
Sun, 20 Mar 2011 21:28:11 +0100 wenzelm structure Timing: covers former start_timing/end_timing and Output.timeit etc;
Mon, 10 Jan 2011 15:45:46 +0100 wenzelm eliminated Int.toString;
Mon, 17 May 2010 23:54:15 +0200 wenzelm prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
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;
Sun, 28 Mar 2010 16:59:06 +0200 wenzelm static defaults for configuration options;
Sun, 07 Mar 2010 12:19:47 +0100 wenzelm modernized structure Object_Logic;
Sat, 06 Mar 2010 15:39:16 +0100 wenzelm eliminated Args.bang_facts (legacy feature);
Sun, 01 Nov 2009 15:44:26 +0100 wenzelm modernized structure Context_Rules;
less more (0) -100 -50 -30 tip