prefer high-level ML_System.share_common_data, ML_System.save_state -- except for bootstrap images (RAW, Pure);

more NEWS;

merge

prove simp theorems for newly generated definitions

example using restoring Transfer/Lifting context

use lifting_forget for deregistering numeric types as a quotient type

restoring Transfer/Lifting context

make ML function for deleting quotients public

public access to the raw transfer rules - for restoring transferring

another move to avoid sporadic kill of poly, which is presumably due to resource management on lxbroy2, lxbroy3 etc.;

more (co)data docs

more (co)data docs

added missing theorems to "simps" collection

more (co)data docs

more (co)data docs

more (co)data docs

merged

tuned proofs;

tuned magic number, for improved reactivity on old 2-core machine;

tuned proofs;

updated keywords

tuned proof

merged

tuned proofs;

print find_thms result in reverse order so best result is on top

more useful sorting of find_thms results

proper sharing after change of directory structure (cf. 32ec957e5c3e); result is structurally equal, despite change of hash key;

restricted heap, which might improve stability of this test;

merged

tuned proofs;

tuned proofs;

updated to jdk-7u40;

added component jdk-7u40.tar.gz (inactive);

merged

more (co)data docs

tuning

more (co)data doc

generalized and simplified proofs of several theorems about convex sets

more (co)data docs

removed accidentally submitted line

more (co)data doc

more general typing of monadic bind

merged

omit automatic Induct.cases_pred declaration, which breaks many existing proofs

NEWS and CONTRIBUTORS

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