| Sun, 11 Nov 2018 16:08:59 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
| Mon, 22 Oct 2018 19:03:47 +0200 |
Manuel Eberl |
Tagged some theories in HOL-Analysis
|
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
|
| Sat, 26 May 2018 22:11:55 +0100 |
paulson |
tidying and reorganisation around Cauchy Integral Theorem
|
file |
diff |
annotate
|
| Mon, 21 May 2018 22:52:16 +0100 |
paulson |
small clean-up of Complex_Analysis_Basics
|
file |
diff |
annotate
|
| Sun, 20 May 2018 18:37:34 +0100 |
paulson |
tidy up of Derivative
|
file |
diff |
annotate
|
| Sun, 29 Apr 2018 14:46:11 +0100 |
paulson |
more defer/prefer
|
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
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Mon, 08 Jan 2018 17:11:25 +0000 |
paulson |
moved in some material from Euler-MacLaurin
|
file |
diff |
annotate
|
| Tue, 12 Dec 2017 10:01:14 +0100 |
Manuel Eberl |
Moved analysis material from AFP
|
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
|
| Tue, 22 Aug 2017 21:36:48 +0200 |
Manuel Eberl |
Lemmas about analysis and permutations
|
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
|
| Tue, 04 Jul 2017 09:36:25 +0100 |
immler |
some generalizations complex=>real_normed_field
|
file |
diff |
annotate
|
| Thu, 15 Jun 2017 17:22:23 +0100 |
paulson |
Some new material. SIMPRULE STATUS for sum/prod.delta rules!
|
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 Oct 2016 15:46:07 +0100 |
paulson |
more new material
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| Fri, 23 Sep 2016 18:34:34 +0200 |
hoelzl |
move absolutely_integrable_on to Equivalence_Lebesgue_Henstock_Integration, now based on the Lebesgue integral
|
file |
diff |
annotate
|
| Mon, 19 Sep 2016 20:06:21 +0200 |
fleury |
left_distrib ~> distrib_right, right_distrib ~> distrib_left
|
file |
diff |
annotate
|
| Fri, 16 Sep 2016 13:56:51 +0200 |
hoelzl |
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
|
file |
diff |
annotate
|
| Mon, 08 Aug 2016 14:13:14 +0200 |
hoelzl |
rename HOL-Multivariate_Analysis to HOL-Analysis.
|
file |
diff |
annotate
| base
|