moved to lxbroy3, hoping that it works better;

separate (semi)ring with normalization

merged

more CONTRIBUTORS;

documentation for 'subgoal' command;

clarified module;

allow to specify suffix of goal parameters;

subgoal parameters are internal by default and named by user;

split multi-goals as usual (outermost Pure.conjunction only);

clarified prems: full subgoal is imported in any case, to avoid remaining schematic variables;

proper state after qed;

clarified keyword categories;

support for subgoal focus command;

tuned;

taylor series with has_integral and integrable_on

merged

no arguments for "standard" (or old "default") methods;

renamed "default" to "standard", to make semantically clear what it is;

tuned;

Merge

Useful lemmas. The theorem concerning swapping the variables in a double integral.

generalized inf and sup_continuous; added intro rules

fix tex-output for rel_mset

removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs

clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c); apply_end cases are no longer seen in current context section (hardly relevant in practice);

improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);

clarified static phase; proper error;

tuned proofs;

more symbols;

more symbols; tuned proofs; tuned ML;

corrected typo

tuned src/HOL/ex/Ballot

add examples from Freek's top 100 theorems (thms 30, 73, 77)

generalized geometric distribution

added lemma

simplified termination criterion for euclidean algorithm (again)

tuned proof

rings follow immediately their corresponding semirings

tuned code setup

algebraic specification for set gcd

premises in 'show' are treated like 'assume';

adapted to a9b71c82647b;

merged

isabelle update_cartouches;

more symbols; eliminated alternative syntax;

tuned proofs;

do not expose goal parameters;

more symbols;

more symbols;

proper spacing, as for other syntax for these symbols;

tuned whitespace;

updated SystemOnTPTP URL

tuned proofs;

merged

implicit goal cases are legacy;

tuned proofs;

more heap -- hoping for more stability of HOL-Proofs;

added method "goals" for proper subgoal cases;

tuned signature;

tuned signature;

tuned;

tuned;

tuned signature;

streamlined definitions and primitive lemma of euclidean algorithm, including code generation

euclidean algorithm on polynomials

more theorems

generalized to definition from literature, which covers also polynomials

put E before (typically remote, hence less reliable) Vampire

tuned proofs -- less digits;

updated to scala-2.11.7;

clarified 'case' command;

silence 'try'

Merge

Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.

tuned proofs;

tuned proofs;

merged

tuned proofs;

tuned proofs;

tuned;

support 'when' statement, which corresponds to 'presume';

added method "sleep";

tuned signature;

tuned whitespace;

clarified nesting of Isar goal structure; tuned message;

tuned;

keep 'Pure.all' in goals when preplaying

use right context for preplay, to avoid errors in fact lookup

reverted some too aggressive TPTP interpreter changes

automatically build image

filter out more Poly/ML messages from (ad hoc) TPTP toools

removed (now illegal) semicolons in generated theory files

use CVC4 instead of CVC3 at CASC

fixed typo

modernized name

more symbols;