Fri, 14 Dec 2012 14:46:01 +0100 hoelzl NEWS
Fri, 14 Dec 2012 12:40:07 +0100 wenzelm merged
Thu, 13 Dec 2012 23:47:01 +0100 blanchet get rid of some junk facts in the MaSh evaluation driver
Thu, 13 Dec 2012 23:22:10 +0100 blanchet generate original name as a comment in SPASS problems as well
Thu, 13 Dec 2012 22:49:08 +0100 blanchet generate comments with original names for debugging
Thu, 13 Dec 2012 22:49:07 +0100 blanchet use MaSh nicknames in ATP problem files to facilitate gathering of statistics
Thu, 13 Dec 2012 22:49:06 +0100 blanchet parallelized MaSh exporter
Thu, 13 Dec 2012 15:39:07 +0100 traytel short library for streams
Thu, 13 Dec 2012 15:36:08 +0100 traytel renamed theory
Thu, 13 Dec 2012 13:11:38 +0100 Christian Sternagel renamed "emb" to "list_hembeq";
Thu, 13 Dec 2012 09:21:45 +0100 blanchet shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
Wed, 12 Dec 2012 22:37:06 +0100 blanchet tuned two lemma names, to avoid name hint clash (which confuses the MaSh evaluation, and which anyway isn't nice or necessary)
Wed, 12 Dec 2012 21:59:03 +0100 blanchet tuning
Wed, 12 Dec 2012 21:48:29 +0100 blanchet tweaked which facts are included for MaSh evaluations
Wed, 12 Dec 2012 21:48:29 +0100 blanchet don't query blacklisted theorems in evaluation driver
Wed, 12 Dec 2012 21:48:29 +0100 blanchet export a pair of ML functions
Fri, 14 Dec 2012 12:18:51 +0100 wenzelm merged;
Fri, 14 Dec 2012 12:16:08 +0100 wenzelm tuned implementation according to Library.insert/merge in ML;
Fri, 14 Dec 2012 12:09:08 +0100 wenzelm more formal class Command.Results;
Thu, 13 Dec 2012 20:39:07 +0100 wenzelm odd bias of sub/superscript keyboard shortcuts -- according to frequency of use;
Thu, 13 Dec 2012 19:53:55 +0100 wenzelm smarter handling of tracing messages: prover process pauses and enters user dialog;
Thu, 13 Dec 2012 18:15:53 +0100 wenzelm tuned;
Thu, 13 Dec 2012 18:00:24 +0100 wenzelm enable Isabelle/ML to produce uninterpreted result messages as well;
Thu, 13 Dec 2012 17:46:33 +0100 wenzelm include command results in tooltip as well;
Thu, 13 Dec 2012 17:29:23 +0100 wenzelm more careful handling of Dialog_Result, with active area and color feedback;
Thu, 13 Dec 2012 13:52:18 +0100 wenzelm identify dialogs via official serial and maintain as result message;
Wed, 12 Dec 2012 23:36:07 +0100 wenzelm rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
Wed, 12 Dec 2012 21:50:42 +0100 wenzelm support dialog via document content;
Wed, 12 Dec 2012 19:03:49 +0100 wenzelm merged
Wed, 12 Dec 2012 15:38:47 +0100 blanchet further fix related to bd9a0028b063 -- that change was per se right, but it exposed a bug in the pattern for "all"
Wed, 12 Dec 2012 15:25:17 +0100 blanchet better tautology check -- don't reject "prod_cases3" for example
Wed, 12 Dec 2012 13:42:14 +0100 blanchet tuned debugging file names
Wed, 12 Dec 2012 17:44:10 +0100 wenzelm more systematic identifier variants to facilitate experimentation;
Wed, 12 Dec 2012 16:28:18 +0100 wenzelm prevent dedicated MacOSX plugin from switching off vital workarounds;
Wed, 12 Dec 2012 14:54:48 +0100 wenzelm improved coupling of zoom_box and scale;
Wed, 12 Dec 2012 13:28:23 +0100 blanchet really all facts means really all facts (well, almost)
Wed, 12 Dec 2012 13:28:01 +0100 blanchet tuning
Wed, 12 Dec 2012 11:56:07 +0100 blanchet use modern SAT solvers with modern Kodkod versions
Wed, 12 Dec 2012 11:18:06 +0100 blanchet got rid of support for Kodkodi < 1.2.14
Wed, 12 Dec 2012 03:47:02 +0100 blanchet made MaSh evaluation driver work with SMT solvers
Wed, 12 Dec 2012 02:47:45 +0100 blanchet merge aliased theorems in MaSh dependencies, modulo symmetry of equality
Wed, 12 Dec 2012 00:24:06 +0100 blanchet adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
Wed, 12 Dec 2012 00:14:58 +0100 blanchet better name for SMT solver files
Wed, 12 Dec 2012 00:14:58 +0100 blanchet updated version of MaSh learner engine
Wed, 12 Dec 2012 00:14:58 +0100 blanchet push normalization further -- avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)
Tue, 11 Dec 2012 22:19:39 +0100 wenzelm disable Find_Unused_Assms_Examples for now, to recover isatest sanity;
Tue, 11 Dec 2012 22:16:23 +0100 wenzelm less massive arrow heads;
Tue, 11 Dec 2012 22:09:22 +0100 wenzelm added explicit zoom box;
Tue, 11 Dec 2012 21:55:56 +0100 wenzelm some attempts at more discrete scale factor;
Tue, 11 Dec 2012 21:28:37 +0100 wenzelm more official graphics context with font metrics;
Tue, 11 Dec 2012 21:05:38 +0100 wenzelm just one class with parameters;
Tue, 11 Dec 2012 12:17:20 +0100 wenzelm initial layout coordinates more like old browser;
Tue, 11 Dec 2012 10:35:42 +0100 wenzelm added speculative options for jEdit;
Mon, 10 Dec 2012 21:55:57 +0100 wenzelm separate instance of class Parameters for each Main_Panel -- avoid global program state;
Mon, 10 Dec 2012 21:28:01 +0100 wenzelm discontinued long names flag -- better done via entity markup, without affecting layout;
Mon, 10 Dec 2012 20:52:57 +0100 wenzelm tuned;
Mon, 10 Dec 2012 20:32:13 +0100 wenzelm tuned;
Mon, 10 Dec 2012 19:58:45 +0100 wenzelm tuned min/max;
Mon, 10 Dec 2012 19:42:58 +0100 wenzelm tuned;
Mon, 10 Dec 2012 19:28:56 +0100 wenzelm keep diagnostic command -- avoid confusion when it disappears;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip