new lemmas

prefer theorem name over 'long_thm_list(n)'

prefer attribute 'unfolded thm' to 'simplified'

removed outdated comments

made non-co case more robust as well (cf. b6e2993fd0d3)

don't wrongly destroy sum types in coiterators

beware of multi-constructor datatypes (cf. 27c418b7b985)

beware of single-constructor datatypes, with no discriminators

more robust tactic to cover another corner case (added as example);

generalized data structure, for extension with SMT solver proofs

prefixed types and some functions with "atp_" for disambiguation

merged;

absorb final CLASSPATH as well, such that tools might provide that by elementary means, without the "classpath" shell function (e.g. kodkodi/nitpick);

more CHECKLIST;

more robust System.getProperty with default;

generate distribution classpath for cold-start application wrappers;

reverse orientation of ISABELLE_CLASSPATH;

propagate ISABELLE_CLASSPATH;

tuned comments;

clarified directory structure;

maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources); ignore $ISABELLE_JAVA_EXT -- do not change java.ext.dirs;

more official initial class path according to sun.misc.Launcher;

provide main classpath again, notably for cold-start;

cold-start of main application even on Linux;

tuned proofs;

more explicit indication of 'done' as proof script element;

made tactic handle gracefully the case: codatatype ('a, 's) scheduler2 = Combine2 "'s => 'a" "'s => ('a, 's) scheduler2"

conceal definitions of high-level constructors and (co)iterators

conceal low-level noted facts (+ FIXME to get rid of the notes altogether eventually)

buffer the notes even more

conceal internal bindings

add a notice to myself in doc

more robust approach to avoid Python byte code -- environment variables get inherited by subprocesses

unset some spurious executable flags

handle corner case in tactic

simplified derivation of in_rel

removed unused/inlinable theorems

when pouring in extra features into the goal, only consider facts from the current theory -- the bottom 10 facts of the last import might be completely unrelated

minor fixes

commented out code parts leading to runtime errors due to missing gensim module

invoke Python with "no bytecode" option to avoid litering Isabelle source directory with ".pyc" files (which can be problematic for a number of reasons)

new version of MaSh

more (co)data docs

avoid a keyword

more (co)datatype docs

killed dead code

get rid of another complication in relevance filter

tuning

renamed config option

more correct NEWS

kick out totally hopeless facts after 5 iterations to speed things up

reintroduced 8d8f72aa5c0b, which does make a small difference in practice, but implemented more efficiently

more (co)data docs

more (co)data docs

more (co)data docs

merged

prefer explicit type constraint (again, see also Type.appl_error); pretty const with markup; clarified "the context";

tuned signature;

tuned whitespace;

tuned message;