2009-02-17 huffman 2009-02-17 remove redundant simp attributes for zdvd rules
2009-02-17 huffman 2009-02-17 lemmas abs_dvd_iff, dvd_abs_iff
2009-02-17 nipkow 2009-02-17 Cleaned up IntDiv and removed subsumed lemmas.
2009-02-16 huffman 2009-02-16 tune section headings; add square function
2009-02-16 huffman 2009-02-16 merged
2009-02-16 huffman 2009-02-16 rearrange subsections
2009-02-16 huffman 2009-02-16 remove instances num::semiring and num::linorder
2009-02-16 huffman 2009-02-16 datatype num = One | Dig0 num | Dig1 num
2009-02-16 huffman 2009-02-16 replace 1::num with One; remove monoid_mult instance
2009-02-15 huffman 2009-02-15 replace dec with double-and-decrement function
2009-02-16 haftmann 2009-02-16 more default simp rules for sgn
2009-02-16 haftmann 2009-02-16 re-generated
2009-02-16 haftmann 2009-02-16 clarified import
2009-02-16 haftmann 2009-02-16 faster preprocessor
2009-02-16 haftmann 2009-02-16 added pdivmod on int (for code generation)
2009-02-16 haftmann 2009-02-16 merged
2009-02-16 haftmann 2009-02-16 tuned texts
2009-02-16 haftmann 2009-02-16 dropped Id
2009-02-16 haftmann 2009-02-16 dropped clause_suc_preproc for generic code generator
2009-02-16 haftmann 2009-02-16 new primrec
2009-02-16 berghofe 2009-02-16 Adapted to encoding of sets as predicates.
2009-02-16 kleing 2009-02-16 enable auto-solve by default
2009-02-16 blanchet 2009-02-16 merged
2009-02-16 blanchet 2009-02-16 Added nitpick attribute, and fixed typo.
2009-02-16 blanchet 2009-02-16 Added myself to testing list.
2009-02-15 nipkow 2009-02-15 dvd and setprod lemmas
2009-02-15 nipkow 2009-02-15 merged
2009-02-15 nipkow 2009-02-15 added finite_set_choice
2009-02-15 krauss 2009-02-15 reject defined function in patterns with errmsg, e.g. f (f x) = x
2009-02-15 nipkow 2009-02-15 fixed document
2009-02-15 nipkow 2009-02-15 more finiteness
2009-02-15 nipkow 2009-02-15 merged
2009-02-15 nipkow 2009-02-15 more finiteness
2009-02-14 nipkow 2009-02-14 merged
2009-02-14 nipkow 2009-02-14 more finiteness
2009-02-14 huffman 2009-02-14 generalize lemma fps_square_eq_iff, move to Ring_and_Field
2009-02-14 huffman 2009-02-14 generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
2009-02-14 huffman 2009-02-14 add mult_delta lemmas; simplify some proofs
2009-02-14 huffman 2009-02-14 fix spelling
2009-02-14 huffman 2009-02-14 declare fps_nth as a typedef morphism; clean up instance proofs
2009-02-14 huffman 2009-02-14 add lemma surj_from_nat
2009-02-14 huffman 2009-02-14 fix document generation
2009-02-14 huffman 2009-02-14 merged
2009-02-14 huffman 2009-02-14 fix document generation
2009-02-13 huffman 2009-02-13 section -> subsection
2009-02-13 huffman 2009-02-13 add instance for cancel_comm_monoid_add
2009-02-13 huffman 2009-02-13 add class cancel_comm_monoid_add
2009-02-14 nipkow 2009-02-14 more finiteness changes
2009-02-13 nipkow 2009-02-13 merged
2009-02-13 nipkow 2009-02-13 finiteness lemmas
2009-02-13 huffman 2009-02-13 merged
2009-02-13 huffman 2009-02-13 unset execute bit
2009-02-13 berghofe 2009-02-13 Tuned datatype antiquotation.
2009-02-13 haftmann 2009-02-13 made SMLNJ happy
2009-02-13 kleing 2009-02-13 typo
2009-02-13 kleing 2009-02-13 find_consts: display the search criteria. (by Timothy Bourke)
2009-02-13 kleing 2009-02-13 find_consts: documentation. (by Timothy Bourke)
2009-02-13 kleing 2009-02-13 FindTheorems solves: update documentation (by Timothy Bourke)
2009-02-13 haftmann 2009-02-13 fixed codegen tool
2009-02-13 haftmann 2009-02-13 merged