src/HOL/Complex.thy
2017-04-26 paulson 2017-04-26 Further new material. The simprule status of some exp and ln identities was reverted.
2017-04-25 paulson 2017-04-25 Fixed LaTeX issue
2017-04-25 paulson 2017-04-25 New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
2017-03-16 paulson 2017-03-16 Removed [simp] status for Complex_eq. Also tidied some proofs
2017-02-28 paulson 2017-02-28 Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands
2017-01-04 paulson 2017-01-04 Many new theorems, and more tidying
2016-10-18 haftmann 2016-10-18 suitable logical type class for abs, sgn
2016-10-17 nipkow 2016-10-17 setprod -> prod
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-07-31 wenzelm 2016-07-31 misc tuning and modernization;
2016-05-23 paulson 2016-05-23 Lots of new material for multivariate analysis
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-03-14 paulson 2016-03-14 New results about paths, segments, etc. The notion of simply_connected.
2016-02-22 paulson 2016-02-22 An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
2016-01-08 hoelzl 2016-01-08 fix code generation for uniformity: uniformity is a non-computable pure data.
2016-01-08 hoelzl 2016-01-08 add uniform spaces
2015-12-30 wenzelm 2015-12-30 more symbols;
2015-12-29 wenzelm 2015-12-29 more symbols;
2015-12-28 wenzelm 2015-12-28 prefer symbols for "abs";
2015-12-15 paulson 2015-12-15 New complex analysis material
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-12-01 paulson 2015-12-01 Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-11-10 paulson 2015-11-10 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-11-02 eberlm 2015-11-02 Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
2015-11-02 eberlm 2015-11-02 Rounding function, uniform limits, cotangent, binomial identities
2015-09-03 paulson 2015-09-03 new lemmas about vector_derivative, complex numbers, paths, etc.
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-06-12 haftmann 2015-06-12 uniform _ div _ as infix syntax for ring division
2015-06-01 haftmann 2015-06-01 separate class for division operator, with particular syntax added in more specific classes
2015-04-11 paulson 2015-04-11 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
2015-03-31 haftmann 2015-03-31 given up separate type classes demanding `inverse 0 = 0`
2015-03-31 paulson 2015-03-31 New material and binomial fix
2015-03-18 paulson 2015-03-18 new HOL Light material about exp, sin, cos
2015-03-18 paulson 2015-03-18 Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
2015-03-09 paulson 2015-03-09 sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
2015-03-05 paulson 2015-03-05 The function frac. Various lemmas about limits, series, the exp function, etc.
2014-11-13 hoelzl 2014-11-13 import general theorems from AFP/Markov_Models
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-21 haftmann 2014-10-21 turn even into an abbreviation
2014-10-19 haftmann 2014-10-19 prefer generic elimination rules for even/odd over specialized unfold rules for nat
2014-09-03 blanchet 2014-09-03 codatatypes are not datatypes
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-16 hoelzl 2014-06-16 add more derivative and continuity rules for complex-values functions
2014-05-07 hoelzl 2014-05-07 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
2014-04-11 nipkow 2014-04-11 made divide_pos_pos a simp rule
2014-04-09 hoelzl 2014-04-09 revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
2014-04-03 paulson 2014-04-03 removing simprule status for divide_minus_left and divide_minus_right
2014-04-03 hoelzl 2014-04-03 merged DERIV_intros, has_derivative_intros into derivative_intros
2014-04-02 hoelzl 2014-04-02 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
2014-03-31 hoelzl 2014-03-31 add complex_of_real coercion
2014-03-21 paulson 2014-03-21 a few new lemmas and generalisations of old ones
2014-03-19 paulson 2014-03-19 Some rationalisation of basic lemmas
2014-02-26 boehmes 2014-02-26 replaced smt-based proof with metis proof that requires no external tool
2014-02-25 paulson 2014-02-25 More complex-related lemmas
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;