prefer implicit build_dialog of isabelle jedit; clarified isabelle build variants; back to $HOME despite some chance that Windows users get it wrong;

offer sessions of group "main" first to increase chances that the user makes a sensible choice;

new contributor

updated README;

HOL-Quickcheck_Benchmark works without timeout (NB: isatest imposes global timeout already);

tuning

merged

reverting d466ebc27810 as the previous changeset should allow to run Find_Unused_Assms_Examples again

providing a custom code equation for vimage to overwrite the vimage definition that would be rewritten by set_comprehension_pointfree simproc in the code preprocessor to an non-terminating code equation

tuned signature: use thy_load to adapt to prover/editor specific view on sources;

tuned property name;

allow to suppress ISABELLE_SYMBOLS for experiments;

escape nicknames

generate proper nicks also for instantiated induction rules

added tracing to ATP exporter

merged

MaSh exporter can now export subsets of the facts, as consecutive ranges

avoid creating nested threads for MaSh -- this seems to cause thread creation failures for machines with dozens of cores (unclear yet if that's really the issue)

thread no timeout properly

proper escaping in file name

encode lemma name in file name

more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment; more tooltip options via Rendering;

prefer more official getMenuShortcutKeyMask, in deviation to traditional jEdit technique;

maintain subtree_elements for improved performance of cumulate operator;

more formal class Markup_Tree.Elements;

tuned command line;

merged

unified layout of defs

tuned;

clarified build_dialog command line;

explicit text_fold markup, which is used by default in Pretty.chunks/chunks2;

updated README;

fold main goal;

fold handling within Pretty_Text_Area, based on formal document content, which is static here; fold subgoals;

tuned signature;

tuned;

tuned error dialog;

init gutter according to view properties, which improves symmetry of windows and allows use of folds etc;

more subgoal markup information, which is potentially useful to manage proof state output;

merged

contribution by A. Colgio

merged

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

actually request heap image in initial up-to-date check;

clarified "isabelle options" command line, to make it more close to "isabelle components";

updated some headers;

clarified README;

more formal components_checksum tool;

just one Admin/components/ directory;

Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors

NEWS

merged

get rid of some junk facts in the MaSh evaluation driver

generate original name as a comment in SPASS problems as well

generate comments with original names for debugging

use MaSh nicknames in ATP problem files to facilitate gathering of statistics

parallelized MaSh exporter

short library for streams

renamed theory

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