Mercurial Mercurial > repos > isabelle / changelog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -24 +24 +50 +100 +300 +1000 +3000 +10000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Wed, 09 Oct 2013 17:21:28 +0200 cleanup SMT-related config options
changeset
blanchet [Wed, 09 Oct 2013 17:21:28 +0200] rev 54094
cleanup SMT-related config options
Wed, 09 Oct 2013 16:40:03 +0200 no isar proofs if preplay was not attempted
changeset
blanchet [Wed, 09 Oct 2013 16:40:03 +0200] rev 54093
no isar proofs if preplay was not attempted
Wed, 09 Oct 2013 16:38:48 +0200 normalize more equalities
changeset
blanchet [Wed, 09 Oct 2013 16:38:48 +0200] rev 54092
normalize more equalities
Wed, 09 Oct 2013 16:07:33 +0200 parallelize MeSh
changeset
blanchet [Wed, 09 Oct 2013 16:07:33 +0200] rev 54091
parallelize MeSh
Wed, 09 Oct 2013 15:58:02 +0200 run relevance filter only once for ATPs and SMT solvers, since it should now yield the same results anyway
changeset
blanchet [Wed, 09 Oct 2013 15:58:02 +0200] rev 54090
run relevance filter only once for ATPs and SMT solvers, since it should now yield the same results anyway
Wed, 09 Oct 2013 15:39:34 +0200 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
changeset
blanchet [Wed, 09 Oct 2013 15:39:34 +0200] rev 54089
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
Wed, 09 Oct 2013 10:47:43 +0200 minor performance tuning
changeset
blanchet [Wed, 09 Oct 2013 10:47:43 +0200] rev 54088
minor performance tuning
Wed, 09 Oct 2013 09:53:18 +0200 use plain types instead of dedicated type pattern
changeset
blanchet [Wed, 09 Oct 2013 09:53:18 +0200] rev 54087
use plain types instead of dedicated type pattern
Wed, 09 Oct 2013 09:51:24 +0200 duplicate term and type patterns
changeset
blanchet [Wed, 09 Oct 2013 09:51:24 +0200] rev 54086
duplicate term and type patterns
Wed, 09 Oct 2013 09:47:59 +0200 optimized built-in const check
changeset
blanchet [Wed, 09 Oct 2013 09:47:59 +0200] rev 54085
optimized built-in const check
Wed, 09 Oct 2013 08:28:36 +0200 added TODO
changeset
blanchet [Wed, 09 Oct 2013 08:28:36 +0200] rev 54084
added TODO
Wed, 09 Oct 2013 08:12:53 +0200 crank up limit a bit -- truly huge background theories are still nearly 3 times larger
changeset
blanchet [Wed, 09 Oct 2013 08:12:53 +0200] rev 54083
crank up limit a bit -- truly huge background theories are still nearly 3 times larger
Tue, 08 Oct 2013 22:33:05 +0200 higher minimum relevance threshold, to prevent Sledgehammer from taking too long on "lemma False"
changeset
blanchet [Tue, 08 Oct 2013 22:33:05 +0200] rev 54082
higher minimum relevance threshold, to prevent Sledgehammer from taking too long on "lemma False"
Tue, 08 Oct 2013 21:19:46 +0200 minor fact filter speedups
changeset
blanchet [Tue, 08 Oct 2013 21:19:46 +0200] rev 54081
minor fact filter speedups
Tue, 08 Oct 2013 20:56:35 +0200 more gracefully handle huge theories in relevance filters
changeset
blanchet [Tue, 08 Oct 2013 20:56:35 +0200] rev 54080
more gracefully handle huge theories in relevance filters
Tue, 08 Oct 2013 20:53:37 +0200 handle huge MaSh requests gracefully
changeset
blanchet [Tue, 08 Oct 2013 20:53:37 +0200] rev 54079
handle huge MaSh requests gracefully
Tue, 08 Oct 2013 16:40:03 +0200 further optimization in relevance filter
changeset
blanchet [Tue, 08 Oct 2013 16:40:03 +0200] rev 54078
further optimization in relevance filter
Tue, 08 Oct 2013 14:53:33 +0200 further speed up duplicate elimination
changeset
blanchet [Tue, 08 Oct 2013 14:53:33 +0200] rev 54077
further speed up duplicate elimination
Tue, 08 Oct 2013 14:41:25 +0200 more efficient theorem variable normalization
changeset
blanchet [Tue, 08 Oct 2013 14:41:25 +0200] rev 54076
more efficient theorem variable normalization
Mon, 07 Oct 2013 23:44:53 +0200 strengthened constructor-view tactic to deal with 'let's
changeset
blanchet [Mon, 07 Oct 2013 23:44:53 +0200] rev 54075
strengthened constructor-view tactic to deal with 'let's
Mon, 07 Oct 2013 23:38:57 +0200 allow 'let's around constructors in constructor view
changeset
blanchet [Mon, 07 Oct 2013 23:38:57 +0200] rev 54074
allow 'let's around constructors in constructor view
Mon, 07 Oct 2013 20:54:55 +0200 reword abstract
changeset
blanchet [Mon, 07 Oct 2013 20:54:55 +0200] rev 54073
reword abstract
Mon, 07 Oct 2013 20:34:16 +0200 more primcorec docs
changeset
blanchet [Mon, 07 Oct 2013 20:34:16 +0200] rev 54072
more primcorec docs
Mon, 07 Oct 2013 20:34:14 +0200 minor doc fix
changeset
blanchet [Mon, 07 Oct 2013 20:34:14 +0200] rev 54071
minor doc fix
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -24 +24 +50 +100 +300 +1000 +3000 +10000 tip
isabelle