src/HOL/Analysis/Complex_Transcendental.thy
Mon, 22 Oct 2018 19:03:47 +0200 Manuel Eberl Tagged some theories in HOL-Analysis
Sat, 04 Aug 2018 01:03:39 +0200 eberlm Small lemmas about analysis
Tue, 03 Jul 2018 14:46:14 +0100 paulson more on infinite products
Fri, 29 Jun 2018 15:22:30 +0100 paulson The unwinding number is an integer.
Thu, 28 Jun 2018 14:13:57 +0100 paulson Generalising and renaming some basic results
Tue, 26 Jun 2018 20:48:49 +0100 paulson a few new lemmas
Tue, 26 Jun 2018 14:51:18 +0100 paulson Rationalisation of complex transcendentals, esp the Arg function
Mon, 25 Jun 2018 12:51:18 +0100 paulson Renaming Arg -> Arg2pi
Thu, 24 May 2018 21:58:17 +0100 paulson more small tidying
Wed, 23 May 2018 21:31:41 +0100 paulson small tidy-up of Complex_Transcendental
Mon, 21 May 2018 22:52:16 +0100 paulson small clean-up of Complex_Analysis_Basics
Thu, 12 Apr 2018 12:16:34 +0100 paulson Analysis builds using set_borel_measurable_def, etc.
Mon, 09 Apr 2018 16:20:23 +0200 nipkow removed dots at the end of (sub)titles
Fri, 23 Feb 2018 13:27:19 +0000 Wenda Li Unified the order of zeros and poles; improved reasoning around non-essential singularites
Thu, 08 Feb 2018 09:19:28 +0100 Manuel Eberl Some lemmas about complex sinh/cosh/tanh
Tue, 16 Jan 2018 09:30:00 +0100 wenzelm standardized towards new-style formal comments: isabelle update_comments;
Mon, 08 Jan 2018 17:11:25 +0000 paulson moved in some material from Euler-MacLaurin
Sun, 24 Dec 2017 14:28:10 +0100 eberlm Removed Analysis/ex/Circle_Area; replaced by more general Analysis/Ball_Volume
Fri, 22 Dec 2017 21:00:07 +0000 paulson new/improved theories involving convergence; better pretty-printing for bounded quantifiers and sum/product
Tue, 05 Dec 2017 12:14:36 +0100 Manuel Eberl Moved material from AFP to Analysis/Number_Theory
Tue, 10 Oct 2017 17:15:37 +0100 paulson Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
Mon, 09 Oct 2017 15:34:23 +0100 paulson new material about connectedness, etc.
Thu, 07 Sep 2017 16:41:40 +0200 nipkow adapted to better linear arith
Mon, 21 Aug 2017 20:49:15 +0200 Manuel Eberl HOL-Analysis: Convergent FPS and infinite sums
Sun, 20 Aug 2017 18:55:03 +0200 Manuel Eberl More lemmas for HOL-Analysis
Fri, 18 Aug 2017 20:47:47 +0200 wenzelm session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
Thu, 17 Aug 2017 14:52:56 +0200 eberlm Replaced subseq with strict_mono
Tue, 04 Jul 2017 09:36:25 +0100 immler some generalizations complex=>real_normed_field
Thu, 04 May 2017 15:14:49 +0100 paulson A few more new lemmas
Thu, 27 Apr 2017 15:59:00 +0100 paulson New material (and some tidying) purely in the Analysis directory
Wed, 26 Apr 2017 16:58:31 +0100 paulson Some fixes related to compactE_image
Wed, 26 Apr 2017 15:53:35 +0100 paulson Further new material. The simprule status of some exp and ln identities was reverted.
Tue, 25 Apr 2017 16:39:54 +0100 paulson New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
Thu, 16 Mar 2017 16:02:18 +0000 paulson Removed [simp] status for Complex_eq. Also tidied some proofs
Tue, 28 Feb 2017 13:51:47 +0000 paulson Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands
Tue, 21 Feb 2017 15:04:01 +0000 paulson Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion
Thu, 05 Jan 2017 16:03:23 +0000 paulson New theory of arcwise connected sets and other new material
Wed, 04 Jan 2017 16:18:50 +0000 paulson Many new theorems, and more tidying
Sat, 17 Dec 2016 15:22:14 +0100 haftmann reoriented congruence rules in non-explosive direction
Sat, 19 Nov 2016 20:10:32 +0100 wenzelm more symbols;
Tue, 25 Oct 2016 15:46:07 +0100 paulson more new material
Tue, 18 Oct 2016 15:55:53 +0100 paulson more from moretop.ml
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Sun, 16 Oct 2016 09:31:04 +0200 haftmann more standardized names
Mon, 19 Sep 2016 20:06:21 +0200 fleury left_distrib ~> distrib_right, right_distrib ~> distrib_left
Thu, 25 Aug 2016 15:50:43 +0200 Manuel Eberl More analysis lemmas
Mon, 08 Aug 2016 14:13:14 +0200 hoelzl rename HOL-Multivariate_Analysis to HOL-Analysis.
less more (0) tip