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;

permissive AList.merge -- most likely setup for theory data (beware of spurious AList.DUP);

provide actual Nitpick_HOL.extended_context;

tuned;

more accurate dependencies;

eliminated obsolete CVS Ids; tuned headers;

merged

added benchmark for large records

merged

clarified quick-and-dirty usage in record package; removed non-optimized versions of proofs; introduced future proofs

simplified bulky metis proofs;

properly inlined @{lemma} antiqutations -- might also reduce proof terms a bit;