2009-02-21 huffman 2009-02-21 fix real_vector, real_algebra instances
2009-02-21 huffman 2009-02-21 merged
2009-02-20 huffman 2009-02-20 generalize lemmas from nat to 'a::wellorder
2009-02-20 huffman 2009-02-20 generalize some lemmas
2009-02-21 nipkow 2009-02-21 merged
2009-02-21 nipkow 2009-02-21 removed redundant thms
2009-02-20 huffman 2009-02-20 merged
2009-02-20 huffman 2009-02-20 class instances for num1
2009-02-20 nipkow 2009-02-20 Removed redundant lemmas
2009-02-20 haftmann 2009-02-20 merged
2009-02-20 haftmann 2009-02-20 also consider superclasses properly
2009-02-20 nipkow 2009-02-20 merged
2009-02-20 nipkow 2009-02-20 removed subsumed lemmas
2009-02-20 haftmann 2009-02-20 merged
2009-02-20 haftmann 2009-02-20 datatype antiquotation: always bracket types with spaces in between
2009-02-20 haftmann 2009-02-20 consequent use of term `code equation`
2009-02-20 haftmann 2009-02-20 permissive check for pattern discipline in case schemes
2009-02-20 haftmann 2009-02-20 maintain order of constructors in datatypes; clarified conventions for type schemes
2009-02-20 haftmann 2009-02-20 stripped Id
2009-02-20 huffman 2009-02-20 merged
2009-02-20 huffman 2009-02-20 add theory of products as real vector spaces to Library
2009-02-20 huffman 2009-02-20 add new theory Product_plus.thy to Library
2009-02-20 immler 2009-02-20 merged
2009-02-20 immler 2009-02-20 changed message
2009-02-20 immler 2009-02-20 detailed information on atp-failure via Output.debug
2009-02-20 haftmann 2009-02-20 merged
2009-02-20 haftmann 2009-02-20 reverted to old wellsorting algorithm
2009-02-20 haftmann 2009-02-20 fixed spurious proof failure
2009-02-20 haftmann 2009-02-20 consider changes variable names in theorem le_imp_power_dvd
2009-02-20 haftmann 2009-02-20 tuned and incremental version of wellsorting algorithm
2009-02-20 haftmann 2009-02-20 ignore sorts in bare types
2009-02-20 haftmann 2009-02-20 defensive implementation of pretty serialisation of lists and characters
2009-02-20 haftmann 2009-02-20 dropped Id
2009-02-20 haftmann 2009-02-20 experimental inclusion of new wellsorting algorithm for code equations
2009-02-20 chaieb 2009-02-20 merged
2009-02-17 chaieb 2009-02-17 merged
2009-02-17 chaieb 2009-02-17 merged
2009-02-17 chaieb 2009-02-17 fixed selection of premises
2009-02-19 huffman 2009-02-19 cleaned up
2009-02-19 huffman 2009-02-19 declare of_int_number_of_eq [simp]
2009-02-19 huffman 2009-02-19 fix case_names
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