Mon, 10 Dec 2012 15:39:20 +0100 wenzelm some clarification for Windows;
Mon, 10 Dec 2012 15:17:47 +0100 wenzelm stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;
Mon, 10 Dec 2012 15:13:13 +0100 wenzelm tuned;
Mon, 10 Dec 2012 13:52:33 +0100 wenzelm generalized notion of active area, where sendback is just one application;
Mon, 10 Dec 2012 14:45:47 +0100 wenzelm merged
Mon, 10 Dec 2012 10:29:52 +0100 blanchet have MaSh evaluator keep all raw problem/solution files in a directory
Mon, 10 Dec 2012 10:41:29 +0100 wenzelm clarified transitive_closure: proper cumulation of transitive steps, which is essential for Warshall-style algorithms;
Sun, 09 Dec 2012 14:05:21 +0100 wenzelm always apply transitive_reduction_acyclic in imitation of old graph browser (essential to avoid slow layout and overcrowded display, e.g. class_deps);
Sun, 09 Dec 2012 14:01:09 +0100 wenzelm added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;
Sat, 08 Dec 2012 22:41:39 +0100 wenzelm merged
Sat, 08 Dec 2012 22:15:44 +0100 blanchet merge
Sat, 08 Dec 2012 21:54:28 +0100 blanchet don't blacklist "case" theorems -- this causes problems in MaSh later
Sat, 08 Dec 2012 13:55:26 +0100 blanchet more changes to MaSh Python program (by Daniel K.)
Sat, 08 Dec 2012 00:48:51 +0100 blanchet don't have MaSh pretend it knows facts it doesn't know
Sat, 08 Dec 2012 00:48:51 +0100 blanchet reverted parallel map idea -- appears to make success rate of ATPs less stable (might even lead to bias in favor of MePo)
Sat, 08 Dec 2012 00:48:50 +0100 blanchet fixed embarrassing off-by-one bug in MaSh's Mesh
Sat, 08 Dec 2012 00:48:50 +0100 blanchet store evaluation output in a file
Sat, 08 Dec 2012 00:48:50 +0100 blanchet use parallel map
Sat, 08 Dec 2012 00:48:50 +0100 blanchet tweak MaSh fudge factors
Sat, 08 Dec 2012 00:48:50 +0100 blanchet more MaSh tweaking -- in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval"
Sat, 08 Dec 2012 22:19:24 +0100 wenzelm basic monitor panel, using the powerful jfreechart library;
Sat, 08 Dec 2012 22:14:39 +0100 wenzelm added jfreechart library, including the old version of iText from its distribution (required for the demo application and examples);
Sat, 08 Dec 2012 13:25:49 +0100 wenzelm check consistent theory names for direct imports as well -- as claimed in the comments (see also 1cc36c0ec9eb);
Fri, 07 Dec 2012 23:14:39 +0100 wenzelm 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);
Fri, 07 Dec 2012 23:11:01 +0100 wenzelm final report_status within SYNCHRONIZED part of scheduler loop: required for sanity of data;
Fri, 07 Dec 2012 20:39:09 +0100 wenzelm adhoc recovery from spurious NPEs, similar quantum-effect behind 7c8ce63a3c00;
Fri, 07 Dec 2012 18:20:33 +0100 wenzelm obsolete;
Fri, 07 Dec 2012 18:05:24 +0100 wenzelm eliminated old copy of proof.sty (1995), prefer the one usually included in current latex distributions (2005);
Fri, 07 Dec 2012 17:00:40 +0100 wenzelm merged
Fri, 07 Dec 2012 16:53:35 +0100 wenzelm deactivate actual fork -- unstable in scala-2.9.2 on multicore hardware;
Fri, 07 Dec 2012 16:33:17 +0100 wenzelm some support to recover from spurious crash -- this is Physics, not Mathematics;
Fri, 07 Dec 2012 16:25:33 +0100 wenzelm 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;
Fri, 07 Dec 2012 16:38:25 +0100 nipkow tuned text
Fri, 07 Dec 2012 15:53:28 +0100 nipkow corrected nonsensical associativity of `` and dvd
Fri, 07 Dec 2012 14:29:09 +0100 hoelzl add exponential and uniform distributions
Fri, 07 Dec 2012 14:29:08 +0100 hoelzl fundamental theorem of calculus for the Lebesgue integral
Fri, 07 Dec 2012 14:28:57 +0100 hoelzl add Int_atMost
Fri, 07 Dec 2012 14:30:00 +0100 wenzelm more rigorous "build only" mode: avoid build dialog of logic image and its potential need for GUI display;
Fri, 07 Dec 2012 13:56:01 +0100 wenzelm fork slow part of Thy_Load.body_files only;
Fri, 07 Dec 2012 13:38:32 +0100 wenzelm explore theory_body_files via future, for improved performance;
Thu, 06 Dec 2012 23:07:10 +0100 wenzelm merged
Thu, 06 Dec 2012 17:48:04 +0100 blanchet use proper entry point for MaSh in test driver
Thu, 06 Dec 2012 16:49:48 +0100 blanchet export ATP and Isar commands separately
Thu, 06 Dec 2012 23:01:49 +0100 wenzelm proper Sendback.markup, as required for standard Prover IDE protocol (see also c62ce309dc26);
Thu, 06 Dec 2012 22:12:25 +0100 wenzelm discontinued obsolete "Tracing" button -- limited tracing channel works sufficiently well;
Thu, 06 Dec 2012 21:54:43 +0100 wenzelm discontinued option jedit_auto_start, which is somewhat pointless as there is no manual session start within Isabelle/jEdit;
Thu, 06 Dec 2012 21:53:35 +0100 wenzelm updated README;
Thu, 06 Dec 2012 21:46:20 +0100 wenzelm documentation for isabelle build_dialog and its implicit use in isabelle jedit;
Thu, 06 Dec 2012 21:16:46 +0100 wenzelm clarified build_dialog: regular up-to-date check (extra cost of approx. 5s startup for HOL);
Thu, 06 Dec 2012 20:26:14 +0100 wenzelm avoid startup within GUI thread -- it is only required later for dialog;
Thu, 06 Dec 2012 17:59:37 +0100 wenzelm more uniform default logic, using settings, options, args etc.;
Thu, 06 Dec 2012 16:07:09 +0100 blanchet use right names in MePo exporter
Thu, 06 Dec 2012 15:54:17 +0100 blanchet parse more liberal MaSh suggestion syntax (for the eval driver)
Thu, 06 Dec 2012 11:42:23 +0100 wenzelm merged
Thu, 06 Dec 2012 11:27:44 +0100 blanchet made Python code compile again (by Daniel K.)
Thu, 06 Dec 2012 11:25:10 +0100 blanchet tweaked MaSh proximity
Thu, 06 Dec 2012 11:25:10 +0100 blanchet reduce max number of dependencies for MaSh to get rid of junk
Thu, 06 Dec 2012 11:25:10 +0100 blanchet more feature tweaks
Thu, 06 Dec 2012 11:25:10 +0100 blanchet prioritize chained facts
Thu, 06 Dec 2012 11:25:10 +0100 blanchet more MaSh feature tweaking
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip