Sun, 06 Nov 2011 14:23:04 +0100 cascading timeouts in minimizer, part 2
blanchet [Sun, 06 Nov 2011 14:23:04 +0100] rev 45372
cascading timeouts in minimizer, part 2
Sun, 06 Nov 2011 14:05:57 +0100 tuning
blanchet [Sun, 06 Nov 2011 14:05:57 +0100] rev 45371
tuning
Sun, 06 Nov 2011 13:57:17 +0100 use "Time.time" rather than milliseconds internally
blanchet [Sun, 06 Nov 2011 13:57:17 +0100] rev 45370
use "Time.time" rather than milliseconds internally
Sun, 06 Nov 2011 13:46:26 +0100 tune: no need for option
blanchet [Sun, 06 Nov 2011 13:46:26 +0100] rev 45369
tune: no need for option
Sun, 06 Nov 2011 13:37:49 +0100 cascading timeouts in minimizer
blanchet [Sun, 06 Nov 2011 13:37:49 +0100] rev 45368
cascading timeouts in minimizer
Sun, 06 Nov 2011 13:32:13 +0100 shortcut binary minimization algorithm
blanchet [Sun, 06 Nov 2011 13:32:13 +0100] rev 45367
shortcut binary minimization algorithm
Sun, 06 Nov 2011 11:51:35 +0100 speed up binary minimizer in practice by preferring the first half of the used facts (which are likelier to be relevant) to the second half
blanchet [Sun, 06 Nov 2011 11:51:35 +0100] rev 45366
speed up binary minimizer in practice by preferring the first half of the used facts (which are likelier to be relevant) to the second half
Sun, 06 Nov 2011 11:16:37 +0100 renamed experimental systems
blanchet [Sun, 06 Nov 2011 11:16:37 +0100] rev 45365
renamed experimental systems
Sun, 06 Nov 2011 11:13:47 +0100 repaired quantification over type variables for non-TFF1/THF encodings
blanchet [Sun, 06 Nov 2011 11:13:47 +0100] rev 45364
repaired quantification over type variables for non-TFF1/THF encodings
Sun, 06 Nov 2011 18:42:15 +0100 misc tuning and modernization;
wenzelm [Sun, 06 Nov 2011 18:42:15 +0100] rev 45363
misc tuning and modernization; more antiquotations;
Sun, 06 Nov 2011 17:53:32 +0100 misc tuning and modernization;
wenzelm [Sun, 06 Nov 2011 17:53:32 +0100] rev 45362
misc tuning and modernization; more antiquotations;
Sun, 06 Nov 2011 17:05:45 +0100 tuned;
wenzelm [Sun, 06 Nov 2011 17:05:45 +0100] rev 45361
tuned;
Sun, 06 Nov 2011 17:00:05 +0100 some statespace benchmarks;
wenzelm [Sun, 06 Nov 2011 17:00:05 +0100] rev 45360
some statespace benchmarks;
Sun, 06 Nov 2011 16:41:53 +0100 write changed .prv files only, to avoid writing into src file-space by default;
wenzelm [Sun, 06 Nov 2011 16:41:53 +0100] rev 45359
write changed .prv files only, to avoid writing into src file-space by default;
Sun, 06 Nov 2011 16:29:22 +0100 tuned document;
wenzelm [Sun, 06 Nov 2011 16:29:22 +0100] rev 45358
tuned document; tuned proofs;
Sun, 06 Nov 2011 16:22:26 +0100 more precise dependencies;
wenzelm [Sun, 06 Nov 2011 16:22:26 +0100] rev 45357
more precise dependencies;
Sun, 06 Nov 2011 14:20:41 +0100 inlined antiquotations;
wenzelm [Sun, 06 Nov 2011 14:20:41 +0100] rev 45356
inlined antiquotations;
Sun, 06 Nov 2011 14:09:24 +0100 misc tuning and modernization;
wenzelm [Sun, 06 Nov 2011 14:09:24 +0100] rev 45355
misc tuning and modernization;
Sun, 06 Nov 2011 13:25:41 +0100 optional timing, to avoid redundant allocation of mutable cells;
wenzelm [Sun, 06 Nov 2011 13:25:41 +0100] rev 45354
optional timing, to avoid redundant allocation of mutable cells;
Sat, 05 Nov 2011 22:41:25 +0100 tuned;
wenzelm [Sat, 05 Nov 2011 22:41:25 +0100] rev 45353
tuned;
Sat, 05 Nov 2011 22:01:19 +0100 misc tuning;
wenzelm [Sat, 05 Nov 2011 22:01:19 +0100] rev 45352
misc tuning;
Sat, 05 Nov 2011 21:36:56 +0100 merged
wenzelm [Sat, 05 Nov 2011 21:36:56 +0100] rev 45351
merged
Sat, 05 Nov 2011 12:01:21 +0000 more use of global operations (see 98ec8b51af9c)
Christian Urban <urbanc@in.tum.de> [Sat, 05 Nov 2011 12:01:21 +0000] rev 45350
more use of global operations (see 98ec8b51af9c)
Sat, 05 Nov 2011 20:40:30 +0100 more uniform instT_subst vs. inst_subst: compare variable names only;
wenzelm [Sat, 05 Nov 2011 20:40:30 +0100] rev 45349
more uniform instT_subst vs. inst_subst: compare variable names only;
Sat, 05 Nov 2011 20:32:12 +0100 tuned cterm_instantiate: avoid somewhat expensive Term.map_types and cterm_of;
wenzelm [Sat, 05 Nov 2011 20:32:12 +0100] rev 45348
tuned cterm_instantiate: avoid somewhat expensive Term.map_types and cterm_of;
Sat, 05 Nov 2011 20:07:38 +0100 misc tuning and modernization;
wenzelm [Sat, 05 Nov 2011 20:07:38 +0100] rev 45347
misc tuning and modernization;
Sat, 05 Nov 2011 19:47:22 +0100 some performance tuning via Term_Subst/Same.operation;
wenzelm [Sat, 05 Nov 2011 19:47:22 +0100] rev 45346
some performance tuning via Term_Subst/Same.operation; tuned;
Sat, 05 Nov 2011 18:58:40 +0100 pruned signature;
wenzelm [Sat, 05 Nov 2011 18:58:40 +0100] rev 45345
pruned signature;
Sat, 05 Nov 2011 15:00:49 +0100 added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm [Sat, 05 Nov 2011 15:00:49 +0100] rev 45344
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types; tuned;
Sat, 05 Nov 2011 10:59:11 +0100 more conventional syntax const;
wenzelm [Sat, 05 Nov 2011 10:59:11 +0100] rev 45343
more conventional syntax const;
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 tip