example tweaking -- also prevents Nitpick_Tests from using more than 1 thread

speed up Nitpick examples a little bit

minor changes

updated example timings

more helpful message

also mention gfp

bump up the max cardinalities, to use up more of the time given to us by the user

make tracing monotonicity easier

more documentation, based on email discussions with a user

make example easier to parse

clarify attribute documentation

choose better example

fix newly introduced bug w.r.t. conditional equations

document something I explained in an email to a poweruser

make Nitpick more flexible when parsing (p)simp rules

fix soundness bug w.r.t. "Suc" with "binary_ints"

handle free variables even more gracefully; 1. show those that only occur in assumptions as part of the constants; 2. make sure locally defined Frees are given an Opt rep, just like constants generally owuld

optimize local "def"s by treating them as definitions

careful about which linear inductive predicates should be starred

help Nitpick

fix Skolemizer -- last week's optimizations resulted in UnequalLengths errors

prevent generation of needless specialized constants etc.

optimize generated Kodkod formula

prefer implication to equality, to be more SAT solver friendly

minor symmetry breaking for codatatypes like llist

fix bug with mutually recursive and nested codatatypes

fix minor bug in sym breaking

modernized specifications; tuned headers;