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;