src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
Sat, 02 Jul 2016 20:22:25 +0200 haftmann simplified definitions of combinatorial functions
Wed, 15 Jun 2016 22:19:03 +0200 hoelzl move open_Collect_eq/less to HOL
Fri, 13 May 2016 20:24:10 +0200 wenzelm eliminated use of empty "assms";
Wed, 09 Mar 2016 17:16:08 +0000 paulson Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
Mon, 07 Mar 2016 15:57:02 +0000 paulson complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
Mon, 07 Mar 2016 14:34:45 +0000 paulson new material to Blochj's theorem, as well as supporting lemmas
Thu, 25 Feb 2016 13:58:48 +0000 paulson Conformal_mappings: a big development in complex analysis (+ some lemmas)
Wed, 24 Feb 2016 15:51:01 +0000 paulson Substantial new material for multivariate analysis. Also removal of some duplicates.
Fri, 22 Jan 2016 16:00:03 +0000 paulson Reorganised a huge proof
Mon, 11 Jan 2016 22:14:15 +0000 paulson nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
Thu, 07 Jan 2016 17:40:55 +0000 paulson revisions to limits and derivatives, plus new lemmas
Wed, 30 Dec 2015 11:37:29 +0100 wenzelm isabelle update_cartouches -c -t;
Wed, 30 Dec 2015 11:21:54 +0100 wenzelm more symbols;
Tue, 29 Dec 2015 23:04:53 +0100 wenzelm more symbols;
Tue, 15 Dec 2015 14:40:36 +0000 paulson New complex analysis material
Mon, 07 Dec 2015 20:19:59 +0100 wenzelm isabelle update_cartouches -c -t;
Mon, 07 Dec 2015 16:44:26 +0000 paulson Cauchy's integral formula for circles. Starting to fix eventually_mono.
Tue, 10 Nov 2015 14:43:29 +0000 paulson Merge
Tue, 10 Nov 2015 14:18:41 +0000 paulson Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
Tue, 03 Nov 2015 16:47:37 +0100 wenzelm tuned imports;
Mon, 02 Nov 2015 11:56:28 +0100 eberlm Rounding function, uniform limits, cotangent, binomial identities
Tue, 27 Oct 2015 15:17:02 +0000 paulson Cauchy's integral formula, required lemmas, and a bit of reorganisation
Mon, 26 Oct 2015 23:41:27 +0000 paulson new lemmas about topology, etc., for Cauchy integral formula
Tue, 22 Sep 2015 16:55:49 +0100 paulson SOME rather than THE makes it easy to prove equivalence with other forms of derivatives
Mon, 31 Aug 2015 21:28:08 +0200 wenzelm prefer symbols;
Fri, 26 Jun 2015 10:20:33 +0200 wenzelm tuned whitespace;
Wed, 10 Jun 2015 19:10:20 +0200 wenzelm isabelle update_cartouches;
Thu, 30 Apr 2015 15:28:01 +0100 paulson tidying some messy proofs
Tue, 28 Apr 2015 16:23:38 +0100 paulson New material about complex transcendental functions (especially Ln, Arg) and polynomials
Sat, 11 Apr 2015 11:56:40 +0100 paulson Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
Mon, 16 Mar 2015 15:30:00 +0000 paulson The factorial function, "fact", now has type "nat => 'a"
Fri, 06 Mar 2015 12:48:03 +0000 paulson A few new lemmas and a bit of tidying up
Wed, 18 Feb 2015 22:46:47 +0100 haftmann inlined rules to free user-space from technical names
Sun, 02 Nov 2014 17:09:04 +0100 wenzelm modernized header;
Sat, 05 Jul 2014 11:01:53 +0200 haftmann prefer ac_simps collections over separate name bindings for add and mult
Wed, 07 May 2014 12:25:35 +0200 hoelzl avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
Wed, 09 Apr 2014 09:37:47 +0200 hoelzl revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
Thu, 03 Apr 2014 23:51:52 +0100 paulson removing simprule status for divide_minus_left and divide_minus_right
Thu, 03 Apr 2014 17:56:08 +0200 hoelzl merged DERIV_intros, has_derivative_intros into derivative_intros
Wed, 02 Apr 2014 18:35:07 +0200 hoelzl extend continuous_intros; remove continuous_on_intros and isCont_intros
Wed, 02 Apr 2014 18:35:02 +0200 hoelzl reorder Complex_Analysis_Basics; rename DD to deriv
Wed, 02 Apr 2014 18:35:01 +0200 hoelzl moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
Mon, 31 Mar 2014 17:17:37 +0200 hoelzl tuned proofs
Mon, 24 Mar 2014 14:22:29 +0000 paulson rearranging some deriv theorems
Fri, 21 Mar 2014 15:36:00 +0000 paulson a few new lemmas and generalisations of old ones
Wed, 19 Mar 2014 20:50:24 -0700 huffman generalize theory of operator norms to work with class real_normed_vector
Wed, 19 Mar 2014 17:06:02 +0000 paulson Some rationalisation of basic lemmas
Wed, 19 Mar 2014 14:54:45 +0000 paulson New complex analysis material
less more (0) tip