merged

added some examples and tests for fun_cases

dropped unnecessary 'open'

tuned headers

moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information; normalized whitespace and indentation

clarified

clarified, dropping unreachable bool special case

dropped dead code

clarified

generate elim rules for elimination of function equalities; added fun_cases command; recover proper cases rules for mutual recursive case (no sum types)

tuned proofs

merged

make 'linear' into a sublocale of 'bounded_linear'; replace 'linear_def' with 'linear_iff'

generalize lemmas

remove unneeded assumption from prime_dvd_power lemmas; add iff forms of prime_dvd_power lemmas (thanks to Jason Dagit)

remove duplicate lemmas

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