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