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;

support to parse obtain clause without type-checking yet; tuned signature;

tuned -- eliminated unused feature;

tuned signature;

tuned;

streamlined many more proofs

Merge

tidied more proofs

proper subclass instances for existing gcd (semi)rings

slight preference for American English

generalized euclidean ring prerequisites

simplified relationship between associated and is_unit

proof tidying

CONTRIBUTORS

tuned lemmas and proofs

given up trivial definition

dropped warnings by dropping ineffective code declarations

standardized algebraic conventions: prefer a, b, c over x, y, z

uniform _ div _ as infix syntax for ring division

fixed several "inside-out" proofs

add transfer theorems for fixed points

Merge

tidied more proofs

misc tuning;

misc tuning;

unused;

misc tuning;

isabelle update_cartouches;

more user aliases;

merged

prefer direct Assumption.add_assms -- avoid term bindings of Proof_Context.add_assms;

tuned proofs;

clarified local after_qed: result is not exported yet; proper goal_export for show: 'if' is like 'assume';

support for "if prems" in local goal statements;

tuned message;

tuned proofs;

no need for protected goal (see 240ad53041c9);

tuned proofs;

prevent export of future result -- avoid interference with goal fixes;

more uniform treatment of auto bindings vs. explicit user bindings; misc tuning;

tuned signature;

allow for_fixes for 'have', 'show' etc.; tuned signature;

eliminated dead code;

clarified abstracted term bindings (again, see c8384ff11711);

tuned signature;

tuned;

clarified term bindings;

tuned

Merge

tuned

Renaming multiset operators < ~> <#,...

more tidying up of proofs

tidying messy proofs

tidying messy proofs

merged

clarified context;

tuned;

clarified abstracted term bindings;

avoid duplicate warning due to Variable.warn_extra_tfrees;

clarified Proof_Context.cert_propp/read_propp; tuned;

more careful treatment of term bindings in 'obtain' proof body; tuned signature;

tuned signature;

Merge

Tidied lots of messy proofs

tuned signature;

tuned (see also 66e6c539a36d);

tuned signature;

clarified: declare props once and for all; tuned signature;

tuned signature;

tuned signature;

tuned signature;

tuned;

tuned;

tuned;

tuned whitespace;

more tight treatment of subgoals: main goal may refer to extra variables;

added Isar command 'supply';

tuned;

clarified signature -- better support for Isar commands outside of Pure;

merged

clarified context;

tuned;

clarified context;

cleaified context; more uniform context data; tuned;

clarified context;

clarified context;

clarified context;

clarified context;

clarified context;

clarified context;

tuned proof;

merged

simps_of_case: Better error if split rule is not an equality

simps_of_case: allow Drule.dummy_thm as ignored split rule

implicit partial divison operation in integral domains

separate class for division operator, with particular syntax added in more specific classes

explicit check for field sort, to anticipate situation where syntactic checking alone will not be sufficient any longer

dropped dead config option

tuned, including proper signature for functor argument

dropped dead code

explicit argument expansion of uncheck rules; rewriting of user-space type system must behave similarly to abbreviations

explicit input marker for operations

completely separated canonical class abbreviations from abbreviations stemming from non-canonical morphisms -- these have no shared concept

self-contained formulation of abbrev for named targets

correct sort constraints for abbreviations in type classes * * * yet another bunch of corrections

separate function to compute exported abbreviation

clearly separated target primitives (target_foo) from self-contained target operations (foo)

tuned order