Added the contributions of Robert Himmelmann to CONTRIBUTIONS and NEWS

Renamed vector_less_eq_def to the more usual name vector_le_def.

merged

replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules

concealing internal definitions of primrec specifications

adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler

changing the proof procedure for parameters; adding a testcase for negation and parameters; adopting print_tac to the latest function print_tac' in the predicate compiler

adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned

check if equations are present for all functions to avoid low-level exception later

anti_sym -> antisym

optionally trace theorems used in proof reconstruction

added arithmetic example using div and mod

bump up Nitpick's axiom/definition unfolding limits, because some real-world problems (e.g. from Boogie) ran into the previous limits; the limits are there to prevent infinite recursion; they can be set arbitrarily high without much harm

merged

comment out debugging code in Nitpick

fixed bug in Nitpick's handling of "The" and "Eps" when the return type is a "bool"

made "NitpickHOL.normalized_rhs_of" more robust in the face of locale definitions

removed "debug := true" that shouldn't have been submitted in the first place

Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)

merged

run Nitpick examples if Kodkodi is available

merged

fixed "expect" of Nitpick examples to reflect latest changes in Nitpick

merged

use SAT solver that's available everywhere for this example

invoke Kodkodi from Nitpick using new $KODKOD/bin/kodkodi script; this requires downloading Kodkodi 1.2.4, or writing a "kodkodi" script that invokes "java de.tum.in.isabelle.Kodkodi.Kodkodi $@"

merged

added constraint for Eq^- in Nitpick's implementation of the monotonicity calculus

change the order in which Nitpick tries SAT solvers; so that the binary JNIs come further down the list and can easily be overridden

Fixed splitting of div and mod on integers (split theorem differed from implementation).

merged

Fixed splitting of div and mod on integers (split theorem differed from implementation).

init_theory: Runtime.controlled_execution for proper exception trace etc.;

eliminated slightly odd name space grouping -- now managed by Isar toplevel;

implicit name space grouping for theory/local_theory transactions;

uniform new_group/reset_group; tuned signature;

eliminated dead code;

generalized procs for rewrite_proof: allow skeleton; fulfill_norm_proof: always normalize result here, no re-normalization after filling;

member/cons: slightly more correct treatment of multi-index, notably empty one;

merged

Fixed a typo in a comment.

Fixed a typo in a comment.

merged

A few more lemmas from Jeremy

removed hassize predicate

Added new lemmas to Euclidean Space by Robert Himmelmann

eliminated obsolete thm position stuff;

tuned signature;

guard future proofs by Goal.future_enabled;

further explosion of HOL-Boogie verification conditions

merged

proper purge

dropped obsolete documentation; updated generated sources

merged

removed a few global names in Nitpick (styp, nat_less, pairf)

add_expand_thm: explicit indication of is_def instead of fragile heuristic, tuned signature; explicit extraction_expand vs. extraction_expand_def attribute;

axiomatization: declare Spec_Rules, direct result;

use simultaneous Morphics.fact;

primitive defs: clarified def (axiom name) vs. description;

eliminated obsolete thm position tags;