2009-02-18 haftmann 2009-02-18 tuned accessor name
2009-02-18 haftmann 2009-02-18 more precise improvement in instantiation user space type system
2009-02-18 haftmann 2009-02-18 do not drop arguments to 0, 1
2009-02-18 haftmann 2009-02-18 merged
2009-02-18 haftmann 2009-02-18 reverted to previous version of Finite_Set.thy
2009-02-18 haftmann 2009-02-18 merged
2009-02-18 haftmann 2009-02-18 merged
2009-02-18 haftmann 2009-02-18 first working version
2009-02-18 haftmann 2009-02-18 tuned comments, stripped ID, deleted superfluous code
2009-02-18 haftmann 2009-02-18 stripped ID
2009-02-18 paulson 2009-02-18 Syntactic support for products over set intervals
2009-02-18 paulson 2009-02-18 No idea what happened here!
2009-02-17 paulson 2009-02-17 Even and odd powers of -1
2009-02-18 blanchet 2009-02-18 merged
2009-02-17 blanchet 2009-02-17 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).
2009-02-16 blanchet 2009-02-16 Added Nitpick tag to 'of_int_of_nat'. This theorem leads to a more efficient encoding to Kodkod than the definition of 'of_int'.
2009-02-17 huffman 2009-02-17 add lemmas for exponentiation
2009-02-17 haftmann 2009-02-17 merged
2009-02-17 haftmann 2009-02-17 unified variable names in case expressions; no exponential fork in translation of case expressions
2009-02-17 huffman 2009-02-17 merged
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