2009-02-19 huffman 2009-02-19 nicer induction/cases rules for numeral types
2009-02-19 huffman 2009-02-19 number_ring instances for numeral types
2009-02-19 huffman 2009-02-19 declare xor_compl_{left,right} [simp]
2009-02-19 huffman 2009-02-19 add rule for minus 1 at type bit
2009-02-19 huffman 2009-02-19 add formalization of a type of integers mod 2 to Library
2009-02-19 huffman 2009-02-19 new theory of real inner product spaces
2009-02-19 huffman 2009-02-19 add Powerdomain_ex.thy
2009-02-19 huffman 2009-02-19 add more ordering lemmas
2009-02-19 huffman 2009-02-19 avoid using ab_semigroup_idem_mult locale for powerdomains
2009-02-19 huffman 2009-02-19 merged
2009-02-18 huffman 2009-02-18 add header
2009-02-18 huffman 2009-02-18 move Polynomial.thy to Library
2009-02-18 huffman 2009-02-18 move FrechetDeriv.thy to Library
2009-02-18 huffman 2009-02-18 split polynomial-related stuff from Deriv.thy into Library/Poly_Deriv.thy
2009-02-19 kleing 2009-02-19 half auto_solve default time out; increase manually in PG for large projects (L4v/Verisoft large).
2009-02-18 huffman 2009-02-18 merged
2009-02-18 huffman 2009-02-18 finish converting Deriv.thy to new polynomial library
2009-02-18 huffman 2009-02-18 generalize int_dvd_cancel_factor simproc to idom class
2009-02-18 huffman 2009-02-18 composition of polynomials
2009-02-18 huffman 2009-02-18 add some lemmas, cleaned up
2009-02-18 huffman 2009-02-18 generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power
2009-02-18 huffman 2009-02-18 move polynomial order stuff from Fundamental_Theorem_Algebra to Polynomial
2009-02-18 huffman 2009-02-18 merged
2009-02-18 huffman 2009-02-18 more subsection headings
2009-02-18 huffman 2009-02-18 speed up proof of exp_exists
2009-02-18 haftmann 2009-02-18 tuned
2009-02-18 haftmann 2009-02-18 sort instances wrt. to class hierarchy
2009-02-18 haftmann 2009-02-18 fixed signature
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