Reintroduce set_interpreter for Collect and op :. I removed them by accident when removing old code that dealt with the "set" type. Incidentally, there is still some broken "set" code in Refute that should be fixed (see TODO in refute.ML).

Added Nitpick tag to 'of_int_of_nat'. This theorem leads to a more efficient encoding to Kodkod than the definition of 'of_int'.

add lemmas for exponentiation

merged

unified variable names in case expressions; no exponential fork in translation of case expressions

merged

remove redundant simp attributes for zdvd rules

lemmas abs_dvd_iff, dvd_abs_iff

Cleaned up IntDiv and removed subsumed lemmas.

tune section headings; add square function

merged

rearrange subsections

remove instances num::semiring and num::linorder

datatype num = One | Dig0 num | Dig1 num

replace 1::num with One; remove monoid_mult instance

replace dec with double-and-decrement function

more default simp rules for sgn

re-generated

clarified import

faster preprocessor

added pdivmod on int (for code generation)

merged

tuned texts

dropped Id

dropped clause_suc_preproc for generic code generator

new primrec

Adapted to encoding of sets as predicates.

enable auto-solve by default

merged

Added nitpick attribute, and fixed typo.