src/HOL/Complex.thy
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2011-09-12 huffman 2011-09-12 move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy
2011-09-08 huffman 2011-09-08 remove unnecessary intermediate lemmas
2011-09-08 huffman 2011-09-08 prove existence, uniqueness, and other properties of complex arg function
2011-09-08 huffman 2011-09-08 tuned
2011-09-08 huffman 2011-09-08 remove obsolete intermediate lemma complex_inverse_complex_split
2011-09-08 huffman 2011-09-08 tuned
2011-09-07 huffman 2011-09-07 add some new lemmas about cis and rcis; simplify some proofs;
2011-09-07 huffman 2011-09-07 Complex.thy: move theorems into appropriate subsections
2011-09-07 huffman 2011-09-07 remove redundant lemma complex_of_real_minus_one
2011-09-07 huffman 2011-09-07 simplify proof of lemma DeMoivre, removing unnecessary intermediate lemma
2011-09-07 huffman 2011-09-07 removed unused lemma sin_cos_squared_add2_mult
2011-09-06 huffman 2011-09-06 remove redundant lemmas i_mult_eq and i_mult_eq2 in favor of i_squared
2011-09-06 huffman 2011-09-06 remove some unnecessary simp rules from simpset
2011-09-06 huffman 2011-09-06 remove redundant lemma real_sum_squared_expand in favor of power2_sum
2011-09-06 huffman 2011-09-06 remove redundant lemma LIMSEQ_Complex in favor of tendsto_Complex
2011-09-05 huffman 2011-09-05 tuned indentation
2011-09-04 huffman 2011-09-04 tuned comments
2011-09-04 huffman 2011-09-04 replace lemma expi_imaginary with reoriented lemma cis_conv_exp
2011-09-04 huffman 2011-09-04 remove redundant lemmas expi_add and expi_zero
2011-08-19 huffman 2011-08-19 move sin_coeff and cos_coeff lemmas to Transcendental.thy; simplify some proofs
2011-08-18 huffman 2011-08-18 define complex exponential 'expi' as abbreviation for 'exp'
2011-08-18 huffman 2011-08-18 remove more bounded_linear locale interpretations (cf. f0de18b62d63)
2011-08-09 huffman 2011-08-09 lemma bounded_linear_intro
2011-08-08 huffman 2011-08-08 standard theorem naming scheme: complex_eqI, complex_eq_iff
2011-03-13 wenzelm 2011-03-13 tuned headers;
2010-07-19 haftmann 2010-07-19 diff_minus subsumes diff_def
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-05-11 huffman 2010-05-11 add lemma tendsto_Complex
2010-05-09 huffman 2010-05-09 avoid using real-specific versions of generic lemmas
2010-04-26 haftmann 2010-04-26 use new classes (linordered_)field_inverse_zero
2010-04-26 haftmann 2010-04-26 class division_ring_inverse_zero
2009-06-07 huffman 2009-06-07 replace 'topo' with 'open'; add extra type constraint for 'open'
2009-06-03 huffman 2009-06-03 more [code del] declarations
2009-06-03 huffman 2009-06-03 replace class open with class topo
2009-06-03 huffman 2009-06-03 introduce class topological_space as a superclass of metric_space
2009-05-28 huffman 2009-05-28 definition of dist for complex
2009-04-29 haftmann 2009-04-29 farewell to class recpower
2009-04-22 haftmann 2009-04-22 power operation defined generic
2009-03-26 wenzelm 2009-03-26 interpretation/interpret: prefixes are mandatory by default;
2009-03-04 huffman 2009-03-04 declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
2008-12-14 ballarin 2008-12-14 Ported HOL and HOL-Library to new locales.
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s