| Fri, 26 Apr 2019 16:51:40 +0100 |
paulson |
Added embedding_map_into_euclideanreal; reduced dependence on Equivalence_Lebesgue_Henstock_Integration in Analysis theories by moving a few lemmas
|
file |
diff |
annotate
|
| Fri, 12 Apr 2019 22:09:25 +0200 |
wenzelm |
modernized tags: default scope excludes proof;
|
file |
diff |
annotate
|
| Tue, 19 Mar 2019 16:14:51 +0000 |
paulson |
new material about topology, etc.; also fixes for yesterday's
|
file |
diff |
annotate
|
| Tue, 22 Jan 2019 12:00:16 +0000 |
paulson |
renamings and new material
|
file |
diff |
annotate
|
| Mon, 14 Jan 2019 18:35:03 +0000 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sat, 29 Dec 2018 16:58:53 +0100 |
nipkow |
more capitalization
|
file |
diff |
annotate
|
| Sat, 29 Dec 2018 15:43:53 +0100 |
nipkow |
capitalize proper names in lemma names
|
file |
diff |
annotate
|
| Fri, 28 Dec 2018 10:29:59 +0100 |
nipkow |
tuned style and headers
|
file |
diff |
annotate
|
| Thu, 27 Dec 2018 19:48:28 +0100 |
nipkow |
tuned headers; ~ -> \<not>
|
file |
diff |
annotate
|
| Sat, 08 Dec 2018 20:27:34 +0000 |
Wenda Li |
Tagged some theories in HOL-Analysis: Cauchy_Integral_Theorem, Riemann_Mapping and Winding_Numbers.
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 14:30:09 +0200 |
nipkow |
Prefix form of infix with * on either side no longer needs special treatment
|
file |
diff |
annotate
|
| Sat, 04 Aug 2018 01:03:39 +0200 |
eberlm |
Small lemmas about analysis
|
file |
diff |
annotate
|
| Sun, 15 Jul 2018 13:15:31 +0100 |
paulson |
more de-applying and a fix
|
file |
diff |
annotate
|
| Thu, 28 Jun 2018 17:14:40 +0100 |
paulson |
Incorporating new/strengthened proofs from Library and AFP entries
|
file |
diff |
annotate
|
| Thu, 28 Jun 2018 14:13:57 +0100 |
paulson |
Generalising and renaming some basic results
|
file |
diff |
annotate
|
| Mon, 25 Jun 2018 12:51:18 +0100 |
paulson |
Renaming Arg -> Arg2pi
|
file |
diff |
annotate
|
| Mon, 11 Jun 2018 22:43:33 +0100 |
paulson |
tidier Cauchy proofs
|
file |
diff |
annotate
|
| Wed, 06 Jun 2018 18:19:55 +0200 |
nipkow |
reorient -> split; documented split
|
file |
diff |
annotate
|
| Mon, 04 Jun 2018 21:00:12 +0100 |
paulson |
more tweaks of Cauchy
|
file |
diff |
annotate
|
| Sat, 02 Jun 2018 22:57:18 +0100 |
paulson |
tidied more Cauchy proofs
|
file |
diff |
annotate
|
| Fri, 01 Jun 2018 09:57:33 +0100 |
paulson |
Fixed latex markup
|
file |
diff |
annotate
|
| Fri, 01 Jun 2018 00:25:23 +0100 |
paulson |
more tidying
|
file |
diff |
annotate
|
| Wed, 30 May 2018 23:11:12 +0100 |
paulson |
winding numbers predicate
|
file |
diff |
annotate
|
| Mon, 28 May 2018 23:15:23 +0100 |
paulson |
more general tidying
|
file |
diff |
annotate
|
| Sun, 27 May 2018 22:56:43 +0100 |
paulson |
tidying up a bit more
|
file |
diff |
annotate
|
| Sat, 26 May 2018 22:11:55 +0100 |
paulson |
tidying and reorganisation around Cauchy Integral Theorem
|
file |
diff |
annotate
|
| Sat, 26 May 2018 08:36:09 +0100 |
paulson |
tidied some proofs
|
file |
diff |
annotate
|
| Tue, 22 May 2018 19:58:17 +0100 |
paulson |
merged
|
file |
diff |
annotate
|
| Mon, 21 May 2018 22:52:16 +0100 |
paulson |
small clean-up of Complex_Analysis_Basics
|
file |
diff |
annotate
|
| Tue, 22 May 2018 14:12:03 +0200 |
nipkow |
removed unicode symbol
|
file |
diff |
annotate
|
| Sun, 20 May 2018 18:37:34 +0100 |
paulson |
tidy up of Derivative
|
file |
diff |
annotate
|
| Thu, 26 Apr 2018 19:51:32 +0200 |
nipkow |
new simp modifier: reorient
|
file |
diff |
annotate
|
| Sat, 14 Apr 2018 09:23:00 +0100 |
paulson |
new material about vec, real^1, etc.
|
file |
diff |
annotate
|
| Mon, 09 Apr 2018 16:20:23 +0200 |
nipkow |
removed dots at the end of (sub)titles
|
file |
diff |
annotate
|
| Thu, 22 Feb 2018 15:17:25 +0100 |
immler |
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
|
file |
diff |
annotate
|
| Thu, 15 Feb 2018 12:11:00 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 09:30:00 +0100 |
wenzelm |
standardized towards new-style formal comments: isabelle update_comments;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 12:35:03 +0100 |
nipkow |
tuned op's
|
file |
diff |
annotate
|
| Thu, 21 Dec 2017 19:09:18 +0100 |
nipkow |
tuned op's
|
file |
diff |
annotate
|
| Thu, 30 Nov 2017 16:59:59 +0100 |
eberlm |
Existence of a holomorphic logarithm
|
file |
diff |
annotate
|
| Thu, 19 Oct 2017 17:16:01 +0100 |
paulson |
Switching to inverse image and constant_on, plus some new material
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Mon, 09 Oct 2017 15:34:23 +0100 |
paulson |
new material about connectedness, etc.
|
file |
diff |
annotate
|
| Fri, 29 Sep 2017 14:12:14 +0100 |
paulson |
New results for Green's theorem
|
file |
diff |
annotate
|
| Mon, 28 Aug 2017 22:31:47 +0100 |
paulson |
final cleanup of negligible_standard_hyperplane and other things
|
file |
diff |
annotate
|
| Fri, 25 Aug 2017 11:10:03 +0100 |
paulson |
renamed s to S to work with previous change
|
file |
diff |
annotate
|
| Mon, 24 Jul 2017 16:50:46 +0100 |
paulson |
refactored some HORRIBLE integration proofs
|
file |
diff |
annotate
|
| Tue, 18 Jul 2017 11:35:32 +0200 |
eberlm |
poles and residues of the Gamma function
|
file |
diff |
annotate
|
| Mon, 26 Jun 2017 16:59:44 +0100 |
paulson |
More tidying of horrible proofs
|
file |
diff |
annotate
|
| Mon, 26 Jun 2017 14:26:03 +0100 |
paulson |
A few renamings and several tidied-up proofs
|
file |
diff |
annotate
|
| Thu, 22 Jun 2017 16:31:29 +0100 |
paulson |
New theorems and much tidying up of the old ones
|
file |
diff |
annotate
|
| Mon, 19 Jun 2017 16:07:47 +0100 |
paulson |
New theorems; stronger theorems; tidier theorems. Also some renaming
|
file |
diff |
annotate
|
| Thu, 27 Apr 2017 15:59:00 +0100 |
paulson |
New material (and some tidying) purely in the Analysis directory
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Tue, 21 Feb 2017 17:12:10 +0000 |
paulson |
some new material, also recasting some theorems using “obtains”
|
file |
diff |
annotate
|
| Tue, 21 Feb 2017 15:04:01 +0000 |
paulson |
Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion
|
file |
diff |
annotate
|
| Thu, 05 Jan 2017 14:18:24 +0000 |
paulson |
New material about path connectedness, etc.
|
file |
diff |
annotate
|
| Wed, 04 Jan 2017 16:18:50 +0000 |
paulson |
Many new theorems, and more tidying
|
file |
diff |
annotate
|