abolished slightly odd global lattice interpretation for min/max

prefer more canonical names for lemmas on min/max

explicit distributivity facts on min/max

postponed min/max lemmas until abstract lattice is available

tuned structure of min/max lemmas

prefer abstract simp rule

more lemmas on abstract lattices

tuning and augmentation of min/max lemmas; more lemmas and simp rules for abstract lattices with order; tuned proofs

more general induction rule; tuned proofs

convenient printing of polynomial values

prefer "Bits" as theory name for abstract bit operations, similar to "Orderings", "Lattices", "Groups" etc.

prefer Y_of_X over X_to_Y; prefer alist over assoc_list; prefer explicit prefix

merge

prevent ambiguity when mutual recursion maps a datatype to itself, which yielded wrong definitions in some cases (e.g. nat)

NEWS

dropped redundant lemma

syntactically tuned

prefer plain bool over dedicated type for binary digits

tuned

compile + reduce problem size by a notch

generate exhaust from nchotomy

made tactic work with theorems with multiple assumptions

renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package)

express weak pullback property of bnfs only in terms of the relator

merged

tuned

reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated)

tuning whitespace