wenzelm [Mon, 10 Dec 2012 20:32:13 +0100] rev 50469
tuned;
wenzelm [Mon, 10 Dec 2012 19:58:45 +0100] rev 50468
tuned min/max;
wenzelm [Mon, 10 Dec 2012 19:42:58 +0100] rev 50467
tuned;
wenzelm [Mon, 10 Dec 2012 19:28:56 +0100] rev 50466
keep diagnostic command -- avoid confusion when it disappears;
wenzelm [Mon, 10 Dec 2012 19:17:16 +0100] rev 50465
tuned;
wenzelm [Mon, 10 Dec 2012 17:44:17 +0100] rev 50464
tuned signature;
wenzelm [Mon, 10 Dec 2012 17:05:51 +0100] rev 50463
removed somewhat pointless Edge_Transitive filter, as the graph is always reduced to its Hasse diagram, to have any chance to layout efficiently;
blanchet [Mon, 10 Dec 2012 16:38:20 +0100] rev 50462
merge
blanchet [Mon, 10 Dec 2012 16:26:23 +0100] rev 50461
merged
blanchet [Mon, 10 Dec 2012 16:20:04 +0100] rev 50460
merge
blanchet [Mon, 10 Dec 2012 13:33:06 +0100] rev 50459
changed capitalization of MeSh filter
blanchet [Mon, 10 Dec 2012 13:02:56 +0100] rev 50458
(re)introduce (even more) aggressive parallelism, for the benefit of those users with dozens of CPU cores
wenzelm [Mon, 10 Dec 2012 16:27:03 +0100] rev 50457
further clarification for Windows;
wenzelm [Mon, 10 Dec 2012 16:07:29 +0100] rev 50456
merged
wenzelm [Mon, 10 Dec 2012 16:06:57 +0100] rev 50455
more generous tracing limit -- rescaled in MB;
wenzelm [Mon, 10 Dec 2012 15:46:50 +0100] rev 50454
recovered title property from bfb5964e3041;
wenzelm [Mon, 10 Dec 2012 15:39:20 +0100] rev 50453
some clarification for Windows;
wenzelm [Mon, 10 Dec 2012 15:17:47 +0100] rev 50452
stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
wenzelm [Mon, 10 Dec 2012 15:13:13 +0100] rev 50451
tuned;
wenzelm [Mon, 10 Dec 2012 13:52:33 +0100] rev 50450
generalized notion of active area, where sendback is just one application;
some support for graphview via active area;
wenzelm [Mon, 10 Dec 2012 14:45:47 +0100] rev 50449
merged
blanchet [Mon, 10 Dec 2012 10:29:52 +0100] rev 50448
have MaSh evaluator keep all raw problem/solution files in a directory
wenzelm [Mon, 10 Dec 2012 10:41:29 +0100] rev 50447
clarified transitive_closure: proper cumulation of transitive steps, which is essential for Warshall-style algorithms;
wenzelm [Sun, 09 Dec 2012 14:05:21 +0100] rev 50446
always apply transitive_reduction_acyclic in imitation of old graph browser (essential to avoid slow layout and overcrowded display, e.g. class_deps);
wenzelm [Sun, 09 Dec 2012 14:01:09 +0100] rev 50445
added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;
wenzelm [Sat, 08 Dec 2012 22:41:39 +0100] rev 50444
merged
blanchet [Sat, 08 Dec 2012 22:15:44 +0100] rev 50443
merge
blanchet [Sat, 08 Dec 2012 21:54:28 +0100] rev 50442
don't blacklist "case" theorems -- this causes problems in MaSh later
blanchet [Sat, 08 Dec 2012 13:55:26 +0100] rev 50441
more changes to MaSh Python program (by Daniel K.)
blanchet [Sat, 08 Dec 2012 00:48:51 +0100] rev 50440
don't have MaSh pretend it knows facts it doesn't know
blanchet [Sat, 08 Dec 2012 00:48:51 +0100] rev 50439
reverted parallel map idea -- appears to make success rate of ATPs less stable (might even lead to bias in favor of MePo)
blanchet [Sat, 08 Dec 2012 00:48:50 +0100] rev 50438
fixed embarrassing off-by-one bug in MaSh's Mesh
blanchet [Sat, 08 Dec 2012 00:48:50 +0100] rev 50437
store evaluation output in a file
blanchet [Sat, 08 Dec 2012 00:48:50 +0100] rev 50436
use parallel map
blanchet [Sat, 08 Dec 2012 00:48:50 +0100] rev 50435
tweak MaSh fudge factors
blanchet [Sat, 08 Dec 2012 00:48:50 +0100] rev 50434
more MaSh tweaking -- in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval"
wenzelm [Sat, 08 Dec 2012 22:19:24 +0100] rev 50433
basic monitor panel, using the powerful jfreechart library;
sorted Isabelle menu entries -- this is mainly a catalog;
wenzelm [Sat, 08 Dec 2012 22:14:39 +0100] rev 50432
added jfreechart library, including the old version of iText from its distribution (required for the demo application and examples);
wenzelm [Sat, 08 Dec 2012 13:25:49 +0100] rev 50431
check consistent theory names for direct imports as well -- as claimed in the comments (see also 1cc36c0ec9eb);
wenzelm [Fri, 07 Dec 2012 23:14:39 +0100] rev 50430
make double-sure that the future scheduler is properly shutdown, otherwise its threads are made persistent and will deadlock with the fresh instance after reloading the image (NB: Present.finish involves another Par_List.map over document_variants and thus might fork again);
wenzelm [Fri, 07 Dec 2012 23:11:01 +0100] rev 50429
final report_status within SYNCHRONIZED part of scheduler loop: required for sanity of data;
wenzelm [Fri, 07 Dec 2012 20:39:09 +0100] rev 50428
adhoc recovery from spurious NPEs, similar quantum-effect behind 7c8ce63a3c00;
wenzelm [Fri, 07 Dec 2012 18:20:33 +0100] rev 50427
obsolete;
wenzelm [Fri, 07 Dec 2012 18:05:24 +0100] rev 50426
eliminated old copy of proof.sty (1995), prefer the one usually included in current latex distributions (2005);
\usepackage{proof} only where required;
wenzelm [Fri, 07 Dec 2012 17:00:40 +0100] rev 50425
merged
wenzelm [Fri, 07 Dec 2012 16:53:35 +0100] rev 50424
deactivate actual fork -- unstable in scala-2.9.2 on multicore hardware;
wenzelm [Fri, 07 Dec 2012 16:33:17 +0100] rev 50423
some support to recover from spurious crash -- this is Physics, not Mathematics;
wenzelm [Fri, 07 Dec 2012 16:25:33 +0100] rev 50422
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time) -- relevant for any application using it, e.g. small paper sessions;
nipkow [Fri, 07 Dec 2012 16:38:25 +0100] rev 50421
tuned text
nipkow [Fri, 07 Dec 2012 15:53:28 +0100] rev 50420
corrected nonsensical associativity of `` and dvd
hoelzl [Fri, 07 Dec 2012 14:29:09 +0100] rev 50419
add exponential and uniform distributions
hoelzl [Fri, 07 Dec 2012 14:29:08 +0100] rev 50418
fundamental theorem of calculus for the Lebesgue integral
hoelzl [Fri, 07 Dec 2012 14:28:57 +0100] rev 50417
add Int_atMost
wenzelm [Fri, 07 Dec 2012 14:30:00 +0100] rev 50416
more rigorous "build only" mode: avoid build dialog of logic image and its potential need for GUI display;
wenzelm [Fri, 07 Dec 2012 13:56:01 +0100] rev 50415
fork slow part of Thy_Load.body_files only;
wenzelm [Fri, 07 Dec 2012 13:38:32 +0100] rev 50414
explore theory_body_files via future, for improved performance;
further internalization of header errors;