src/HOL/Real_Vector_Spaces.thy
Mon, 01 Apr 2019 17:02:43 +0100 paulson A few results in Algebra, and bits for Analysis
Mon, 21 Jan 2019 14:44:23 +0000 paulson new material about summations and powers, along with some tweaks
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Thu, 27 Dec 2018 21:32:36 +0100 immler moved lemmas up
Thu, 27 Dec 2018 21:32:34 +0100 immler prove lemmas in context real_normed_vector
Thu, 08 Nov 2018 09:11:52 +0100 haftmann removed relics of ASCII syntax for indexed big operators
Mon, 24 Sep 2018 14:30:09 +0200 nipkow Prefix form of infix with * on either side no longer needs special treatment
Sat, 04 Aug 2018 01:03:39 +0200 eberlm Small lemmas about analysis
Sat, 21 Jul 2018 13:30:43 +0200 paulson de-applying and removing junk
Wed, 11 Jul 2018 19:19:00 +0100 paulson de-applying
Thu, 05 Jul 2018 23:37:00 +0100 paulson de-applying
Thu, 28 Jun 2018 17:14:40 +0100 paulson Incorporating new/strengthened proofs from Library and AFP entries
Tue, 26 Jun 2018 14:51:18 +0100 paulson Rationalisation of complex transcendentals, esp the Arg function
Mon, 18 Jun 2018 14:22:26 +0100 paulson New material in support of quaternions
Wed, 06 Jun 2018 14:22:54 +0200 wenzelm isabelle update_comments;
Wed, 02 May 2018 13:49:38 +0200 immler added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
Mon, 26 Feb 2018 07:34:05 +0100 immler moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
Fri, 23 Feb 2018 13:27:19 +0000 Wenda Li Unified the order of zeros and poles; improved reasoning around non-essential singularites
Mon, 19 Feb 2018 16:44:45 +0000 paulson lots of new material, ultimately related to measure theory
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Tue, 05 Dec 2017 12:14:36 +0100 Manuel Eberl Moved material from AFP to Analysis/Number_Theory
Mon, 09 Oct 2017 15:34:23 +0100 paulson new material about connectedness, etc.
Mon, 14 Aug 2017 19:17:07 +0100 paulson patching the previous commit
Mon, 14 Aug 2017 18:54:25 +0100 paulson further Hensock tidy-up
Thu, 15 Jun 2017 17:22:23 +0100 paulson Some new material. SIMPRULE STATUS for sum/prod.delta rules!
Tue, 02 May 2017 14:34:06 +0100 paulson Simplification of some proofs. Also key lemmas using !! rather than ! in premises
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
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 14:18:24 +0000 paulson New material about path connectedness, etc.
Mon, 17 Oct 2016 17:33:07 +0200 nipkow setprod -> prod
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Sun, 16 Oct 2016 09:31:04 +0200 haftmann more standardized names
Fri, 30 Sep 2016 14:05:51 +0100 paulson new material on paths, etc. Also rationalisation
Wed, 21 Sep 2016 14:20:07 +0100 paulson vector_add_divide_simps now a "named theorems" bundle
Sun, 18 Sep 2016 20:33:48 +0200 wenzelm tuned proofs;
Fri, 12 Aug 2016 17:53:55 +0200 wenzelm more symbols;
Thu, 28 Jul 2016 17:16:16 +0200 immler numerical bounds on pi
Fri, 22 Jul 2016 21:43:56 +0200 wenzelm misc tuning and modernization;
Wed, 13 Jul 2016 17:14:17 +0100 paulson lots of new theorems about differentiable_on, retracts, ANRs, etc.
Tue, 24 May 2016 13:57:34 +0100 paulson renamings and new material
Mon, 23 May 2016 15:33:24 +0100 paulson Lots of new material for multivariate analysis
Mon, 25 Apr 2016 16:09:26 +0200 wenzelm eliminated old 'def';
Mon, 11 Apr 2016 16:27:42 +0100 paulson lots of new theorems for multivariate analysis
Tue, 15 Mar 2016 14:08:25 +0000 paulson rationalisation of theorem names esp about "real Archimedian" etc.
Mon, 07 Mar 2016 14:34:45 +0000 paulson new material to Blochj's theorem, as well as supporting lemmas
Wed, 24 Feb 2016 15:51:01 +0000 paulson Substantial new material for multivariate analysis. Also removal of some duplicates.
Mon, 22 Feb 2016 14:37:56 +0000 paulson An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
Mon, 08 Feb 2016 19:53:49 +0100 hoelzl add type class for topological monoids
Wed, 17 Feb 2016 21:51:57 +0100 haftmann generalized some lemmas;
Mon, 11 Jan 2016 22:14:15 +0000 paulson nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
Fri, 08 Jan 2016 17:41:04 +0100 hoelzl fix code generation for uniformity: uniformity is a non-computable pure data.
Fri, 08 Jan 2016 17:40:59 +0100 hoelzl add uniform spaces
Thu, 07 Jan 2016 17:40:55 +0000 paulson revisions to limits and derivatives, plus new lemmas
Mon, 04 Jan 2016 17:45:36 +0100 eberlm Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
Wed, 30 Dec 2015 14:05:51 +0100 wenzelm more symbols;
Wed, 30 Dec 2015 11:21:54 +0100 wenzelm more symbols;
Tue, 29 Dec 2015 23:04:53 +0100 wenzelm more symbols;
Sun, 27 Dec 2015 21:46:36 +0100 wenzelm prefer symbols for "floor", "ceiling";
Wed, 23 Dec 2015 14:36:45 +0100 immler transfer rule for bounded_linear of blinfun
less more (0) -100 -60 tip