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;