tuned signature;

generalized sup_continuty of add, ereal_of_enat

add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer

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;

tuned proofs;

tuned proofs;

eliminated list_all;

tuned proofs;

tuned proofs;

tuned proofs;

isabelle update_cartouches;

misc tuning;

less ambitious USER_HOME on Windows: avoid potentially disconnected share, agree with guess of JVM user.home;

isabelle update_cartouches;

avoid suspicious Unicode;

tuned;

tuned proofs;

isabelle update_cartouches;

merged

removed dead code;

discontinued unused 'defer_recdef';

tuned;

removed dead code;

moved sources;

tuned proofs;

uniform system_mode for build test: avoid spurious output_dir/log that is not required later;

separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial

generalized some theorems about integral domains and moved to HOL theories

renamed multiset_of -> mset

NEWS

multiset_of_set -> mset_set

tuned proofs -- slightly faster;

merged

tuned proofs -- slightly faster;

tuned proofs -- much faster;

tuned proofs;

tuned

merged

added funs and lemmas

tuned proofs;

merged

manual merge;

tuned proofs;

isabelle update_cartouches;

avoid dynamic parsing of hardwired strings;

more compact name

NEWS

merged

renamed Multiset.set_of to the canonical set_mset

correccted the pretty-printing specs for setsum and setprod

New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.

another messy proof fixed

merged

more informative check: dummies are always allowed parse_term and should not lead to rejection here;

vacuous fact `TERM x`;

tuned signature;

inverted another messy proof

redundant: read = check o parse;

tuned;

moved sections;

moved sections;

tuned;

more robust: variables need not occur in body;

tuned;

tuned whitespace;

merged

improved treatment of Element.Obtains via Expression.prepare_stmt; discontinued pointless all_types ctxt: prep_var is always sequential;

clarified context; tuned;

tuned comment;

another tangled proof

Merge

Tidied up more proofs

merged

more examples;

tuned signature;

tuned;

another proof

fixing more proofs

Merge

Merge

fixed another horrible proof

tuned proofs;

tuned signature;

merged

more on 'consider' and related concepts;

tuned proofs;

tuned proofs;

open parameters for 'consider' rule;

implicit rule for method "cases";

eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;

clarified 'obtain', using structured 'have' statement;

tuned comments;

clarified 'consider', using structured 'have' statement;

more examples;

renamed "prems" to "that";

support for 'consider' command; allow full "fixes" for 'obtain' command; tuned signature;

made SML/NJ happy;