2007-05-24 nipkow 2007-05-24 *** empty log message ***
2007-05-24 obua 2007-05-24 Squared things out.
2007-05-24 narboux 2007-05-24 fix a bug : the semantics of no_asm was the opposite
2007-05-24 urbanc 2007-05-24 temporary fix for a bug in fresh_fun_simp
2007-05-24 urbanc 2007-05-24 formalisation of my PhD (the result was correct, but the proof needed several corrections)
2007-05-24 narboux 2007-05-24 add an option in fresh_fun_simp to prevent rewriting in assumptions
2007-05-24 haftmann 2007-05-24 fixes tvar issue in type inference
2007-05-24 haftmann 2007-05-24 tuned
2007-05-24 haftmann 2007-05-24 tuned warning
2007-05-24 haftmann 2007-05-24 rudimentary class target implementation
2007-05-24 haftmann 2007-05-24 tuned Pure/General/name_space.ML
2007-05-24 nipkow 2007-05-24 Introduced new classes monoid_add and group_add
2007-05-23 huffman 2007-05-23 add lemma complete_algebra_summable_geometric
2007-05-23 paulson 2007-05-23 formatting
2007-05-23 huffman 2007-05-23 generalize powerseries and termdiffs lemmas using axclasses
2007-05-23 huffman 2007-05-23 remove unused simproc definition
2007-05-23 huffman 2007-05-23 remove redundant simproc; remove legacy ML bindings
2007-05-23 huffman 2007-05-23 remove redundant simproc
2007-05-22 huffman 2007-05-22 new simp rule Infinitesimal_of_hypreal_iff
2007-05-22 huffman 2007-05-22 removed redundant lemmas
2007-05-22 huffman 2007-05-22 generalize uniqueness of limits to class real_normed_algebra_1
2007-05-22 paulson 2007-05-22 Some hacks for SPASS format
2007-05-22 krauss 2007-05-22 some optimizations, cleanup
2007-05-22 huffman 2007-05-22 add missing instance declarations
2007-05-22 haftmann 2007-05-22 adjusted to change in Provers/Arith/combine_numerals.ML
2007-05-22 haftmann 2007-05-22 adjusted to change in Provers/Arith/combine_numerals.ML
2007-05-22 krauss 2007-05-22 regression tests: send failure reports to krauss@in.tum.de, too
2007-05-22 huffman 2007-05-22 rename lemmas LIM_ident, isCont_ident, DERIV_ident
2007-05-22 huffman 2007-05-22 remove obsolete CSeries.thy
2007-05-22 huffman 2007-05-22 generalized ring_eq_cancel simprocs to class idom; removed redundant field_eq_cancel simprocs
2007-05-21 huffman 2007-05-21 new field_combine_numerals simproc, which uses fractions as coefficients
2007-05-21 narboux 2007-05-21 search bottom up to get the inner fresh fun
2007-05-21 narboux 2007-05-21 add a bottom up search function
2007-05-21 haftmann 2007-05-21 tuned
2007-05-21 haftmann 2007-05-21 evaluation for integers
2007-05-21 haftmann 2007-05-21 added lemma divAlg_div_mof
2007-05-21 haftmann 2007-05-21 improved code for rev
2007-05-21 haftmann 2007-05-21 min/max
2007-05-21 huffman 2007-05-21 generalize CombineNumerals functor to allow coefficients with types other than IntInf.int
2007-05-21 huffman 2007-05-21 add lemmas divide_numeral_1 and inverse_numeral_1
2007-05-21 krauss 2007-05-21 fixed signature
2007-05-21 krauss 2007-05-21 Method "lexicographic_order" now takes the same arguments as "auto"
2007-05-21 narboux 2007-05-21 change fresh_fun_simp to treat occurences in assumptions and try to solve the generated subgoals
2007-05-20 huffman 2007-05-20 define pi with THE instead of SOME; cleaned up
2007-05-20 huffman 2007-05-20 add lemmas for sin,cos,tan of 30,45,60 degrees; cleaned up
2007-05-20 huffman 2007-05-20 add lemma power2_eq_imp_eq
2007-05-20 urbanc 2007-05-20 added lemma for permutations on strings
2007-05-20 huffman 2007-05-20 moved sqrt lemmas from Transcendental.thy to NthRoot.thy
2007-05-20 huffman 2007-05-20 remove obsolete DERIV_ln lemmas
2007-05-20 huffman 2007-05-20 add realpow_pos_nth2 back in
2007-05-20 huffman 2007-05-20 add odd_real_root lemmas
2007-05-20 huffman 2007-05-20 add lemmas about inverse functions; cleaned up proof of polar_ex
2007-05-20 huffman 2007-05-20 change premises of DERIV_inverse_function lemma
2007-05-20 huffman 2007-05-20 rearranged sections
2007-05-20 huffman 2007-05-20 add lemmas about continuity and derivatives of roots
2007-05-20 huffman 2007-05-20 add lemma DERIV_inverse_function
2007-05-20 huffman 2007-05-20 add lemmas LIM_compose2, isCont_LIM_compose2
2007-05-19 haftmann 2007-05-19 improved aliassing
2007-05-19 haftmann 2007-05-19 more robust thm handling
2007-05-19 chaieb 2007-05-19 added a set of NNF normalization lemmas and nnf_conv