2012-12-13 traytel 2012-12-13 renamed theory
2012-12-13 Christian Sternagel 2012-12-13 renamed "emb" to "list_hembeq"; make "list_hembeq" reflexive independent of the base order; renamed "sub" to "sublisteq"; dropped "transp_on" (state transitivity explicitly instead); no need to hide "sub" after renaming; replaced some ASCII symbols by proper Isabelle symbols; NEWS
2012-12-13 blanchet 2012-12-13 shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
2012-12-12 blanchet 2012-12-12 tuned two lemma names, to avoid name hint clash (which confuses the MaSh evaluation, and which anyway isn't nice or necessary)
2012-12-12 blanchet 2012-12-12 tuning
2012-12-12 blanchet 2012-12-12 tweaked which facts are included for MaSh evaluations
2012-12-12 blanchet 2012-12-12 don't query blacklisted theorems in evaluation driver
2012-12-12 blanchet 2012-12-12 export a pair of ML functions
2012-12-14 wenzelm 2012-12-14 merged;
2012-12-14 wenzelm 2012-12-14 tuned implementation according to Library.insert/merge in ML;
2012-12-14 wenzelm 2012-12-14 more formal class Command.Results;
2012-12-13 wenzelm 2012-12-13 odd bias of sub/superscript keyboard shortcuts -- according to frequency of use;
2012-12-13 wenzelm 2012-12-13 smarter handling of tracing messages: prover process pauses and enters user dialog;
2012-12-13 wenzelm 2012-12-13 tuned;
2012-12-13 wenzelm 2012-12-13 enable Isabelle/ML to produce uninterpreted result messages as well;
2012-12-13 wenzelm 2012-12-13 include command results in tooltip as well;
2012-12-13 wenzelm 2012-12-13 more careful handling of Dialog_Result, with active area and color feedback; more formal type Command.Results; propagate command results to output, which is required to resolve update of dialog state; clarified Markup.message: retain uninterpreted messages;
2012-12-13 wenzelm 2012-12-13 identify dialogs via official serial and maintain as result message; clarified Protocol.is_inlined: suppress result/tracing/state messages uniformly; cumulate_markup/select_markup depending on command state; explicit Rendering.output_messages; tuned source structure;
2012-12-12 wenzelm 2012-12-12 rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
2012-12-12 wenzelm 2012-12-12 support dialog via document content;
2012-12-12 wenzelm 2012-12-12 merged
2012-12-12 blanchet 2012-12-12 further fix related to bd9a0028b063 -- that change was per se right, but it exposed a bug in the pattern for "all"
2012-12-12 blanchet 2012-12-12 better tautology check -- don't reject "prod_cases3" for example
2012-12-12 blanchet 2012-12-12 tuned debugging file names
2012-12-12 wenzelm 2012-12-12 more systematic identifier variants to facilitate experimentation;
2012-12-12 wenzelm 2012-12-12 prevent dedicated MacOSX plugin from switching off vital workarounds;
2012-12-12 wenzelm 2012-12-12 improved coupling of zoom_box and scale; explicit rescale(1.0) on startup;
2012-12-12 blanchet 2012-12-12 really all facts means really all facts (well, almost)
2012-12-12 blanchet 2012-12-12 tuning
2012-12-12 blanchet 2012-12-12 use modern SAT solvers with modern Kodkod versions
2012-12-12 blanchet 2012-12-12 got rid of support for Kodkodi < 1.2.14
2012-12-12 blanchet 2012-12-12 made MaSh evaluation driver work with SMT solvers
2012-12-12 blanchet 2012-12-12 merge aliased theorems in MaSh dependencies, modulo symmetry of equality
2012-12-12 blanchet 2012-12-12 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
2012-12-12 blanchet 2012-12-12 better name for SMT solver files
2012-12-12 blanchet 2012-12-12 updated version of MaSh learner engine
2012-12-12 blanchet 2012-12-12 push normalization further -- avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.)
2012-12-11 wenzelm 2012-12-11 disable Find_Unused_Assms_Examples for now, to recover isatest sanity;
2012-12-11 wenzelm 2012-12-11 less massive arrow heads;
2012-12-11 wenzelm 2012-12-11 added explicit zoom box;
2012-12-11 wenzelm 2012-12-11 some attempts at more discrete scale factor;
2012-12-11 wenzelm 2012-12-11 more official graphics context with font metrics;
2012-12-11 wenzelm 2012-12-11 just one class with parameters;
2012-12-11 wenzelm 2012-12-11 initial layout coordinates more like old browser; tuned geometry defaults;
2012-12-11 wenzelm 2012-12-11 added speculative options for jEdit;
2012-12-10 wenzelm 2012-12-10 separate instance of class Parameters for each Main_Panel -- avoid global program state; misc tuning;
2012-12-10 wenzelm 2012-12-10 discontinued long names flag -- better done via entity markup, without affecting layout;
2012-12-10 wenzelm 2012-12-10 tuned;
2012-12-10 wenzelm 2012-12-10 tuned;
2012-12-10 wenzelm 2012-12-10 tuned min/max;
2012-12-10 wenzelm 2012-12-10 tuned;
2012-12-10 wenzelm 2012-12-10 keep diagnostic command -- avoid confusion when it disappears;
2012-12-10 wenzelm 2012-12-10 tuned;
2012-12-10 wenzelm 2012-12-10 tuned signature;
2012-12-10 wenzelm 2012-12-10 removed somewhat pointless Edge_Transitive filter, as the graph is always reduced to its Hasse diagram, to have any chance to layout efficiently;
2012-12-10 blanchet 2012-12-10 merge
2012-12-10 blanchet 2012-12-10 merged
2012-12-10 blanchet 2012-12-10 merge
2012-12-10 blanchet 2012-12-10 changed capitalization of MeSh filter
2012-12-10 blanchet 2012-12-10 (re)introduce (even more) aggressive parallelism, for the benefit of those users with dozens of CPU cores