better tautology check -- don't reject "prod_cases3" for example

tuned debugging file names

more systematic identifier variants to facilitate experimentation;

prevent dedicated MacOSX plugin from switching off vital workarounds;

improved coupling of zoom_box and scale; explicit rescale(1.0) on startup;

really all facts means really all facts (well, almost)

tuning

use modern SAT solvers with modern Kodkod versions

got rid of support for Kodkodi < 1.2.14

made MaSh evaluation driver work with SMT solvers

merge aliased theorems in MaSh dependencies, modulo symmetry of equality

adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)

better name for SMT solver files

updated version of MaSh learner engine

push normalization further -- avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)

disable Find_Unused_Assms_Examples for now, to recover isatest sanity;

less massive arrow heads;

added explicit zoom box;

some attempts at more discrete scale factor;

more official graphics context with font metrics;

just one class with parameters;

initial layout coordinates more like old browser; tuned geometry defaults;

added speculative options for jEdit;

separate instance of class Parameters for each Main_Panel -- avoid global program state; misc tuning;

discontinued long names flag -- better done via entity markup, without affecting layout;

tuned;

tuned;

tuned min/max;

tuned;

keep diagnostic command -- avoid confusion when it disappears;

tuned;

tuned signature;

removed somewhat pointless Edge_Transitive filter, as the graph is always reduced to its Hasse diagram, to have any chance to layout efficiently;

merge

merged

merge

changed capitalization of MeSh filter

(re)introduce (even more) aggressive parallelism, for the benefit of those users with dozens of CPU cores

further clarification for Windows;

merged

more generous tracing limit -- rescaled in MB;

recovered title property from bfb5964e3041;

some clarification for Windows;

stateless dockable window for graphview, which is triggered by the active area of the corresponding diagnostic command;

tuned;

generalized notion of active area, where sendback is just one application; some support for graphview via active area;

merged

have MaSh evaluator keep all raw problem/solution files in a directory

clarified transitive_closure: proper cumulation of transitive steps, which is essential for Warshall-style algorithms;

always apply transitive_reduction_acyclic in imitation of old graph browser (essential to avoid slow layout and overcrowded display, e.g. class_deps);

added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;

merged

merge

don't blacklist "case" theorems -- this causes problems in MaSh later

more changes to MaSh Python program (by Daniel K.)

don't have MaSh pretend it knows facts it doesn't know

reverted parallel map idea -- appears to make success rate of ATPs less stable (might even lead to bias in favor of MePo)

fixed embarrassing off-by-one bug in MaSh's Mesh

store evaluation output in a file

use parallel map