| Sat, 02 Jul 2016 20:22:25 +0200 |
haftmann |
simplified definitions of combinatorial functions
|
file |
diff |
annotate
|
| Wed, 15 Jun 2016 22:19:03 +0200 |
hoelzl |
move open_Collect_eq/less to HOL
|
file |
diff |
annotate
|
| Fri, 13 May 2016 20:24:10 +0200 |
wenzelm |
eliminated use of empty "assms";
|
file |
diff |
annotate
|
| Wed, 09 Mar 2016 17:16:08 +0000 |
paulson |
Wenda Li's new material: residue theorem, argument_principle, Rouche_theorem
|
file |
diff |
annotate
|
| Mon, 07 Mar 2016 15:57:02 +0000 |
paulson |
complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
|
file |
diff |
annotate
|
| Mon, 07 Mar 2016 14:34:45 +0000 |
paulson |
new material to Blochj's theorem, as well as supporting lemmas
|
file |
diff |
annotate
|
| Thu, 25 Feb 2016 13:58:48 +0000 |
paulson |
Conformal_mappings: a big development in complex analysis (+ some lemmas)
|
file |
diff |
annotate
|
| Wed, 24 Feb 2016 15:51:01 +0000 |
paulson |
Substantial new material for multivariate analysis. Also removal of some duplicates.
|
file |
diff |
annotate
|
| Fri, 22 Jan 2016 16:00:03 +0000 |
paulson |
Reorganised a huge proof
|
file |
diff |
annotate
|
| Mon, 11 Jan 2016 22:14:15 +0000 |
paulson |
nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 17:40:55 +0000 |
paulson |
revisions to limits and derivatives, plus new lemmas
|
file |
diff |
annotate
|
| Wed, 30 Dec 2015 11:37:29 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 30 Dec 2015 11:21:54 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 29 Dec 2015 23:04:53 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 15 Dec 2015 14:40:36 +0000 |
paulson |
New complex analysis material
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 20:19:59 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 16:44:26 +0000 |
paulson |
Cauchy's integral formula for circles. Starting to fix eventually_mono.
|
file |
diff |
annotate
|
| Tue, 10 Nov 2015 14:43:29 +0000 |
paulson |
Merge
|
file |
diff |
annotate
|
| Tue, 10 Nov 2015 14:18:41 +0000 |
paulson |
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
|
file |
diff |
annotate
|
| Tue, 03 Nov 2015 16:47:37 +0100 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
| Mon, 02 Nov 2015 11:56:28 +0100 |
eberlm |
Rounding function, uniform limits, cotangent, binomial identities
|
file |
diff |
annotate
|
| Tue, 27 Oct 2015 15:17:02 +0000 |
paulson |
Cauchy's integral formula, required lemmas, and a bit of reorganisation
|
file |
diff |
annotate
|
| Mon, 26 Oct 2015 23:41:27 +0000 |
paulson |
new lemmas about topology, etc., for Cauchy integral formula
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 16:55:49 +0100 |
paulson |
SOME rather than THE makes it easy to prove equivalence with other forms of derivatives
|
file |
diff |
annotate
|
| Mon, 31 Aug 2015 21:28:08 +0200 |
wenzelm |
prefer symbols;
|
file |
diff |
annotate
|
| Fri, 26 Jun 2015 10:20:33 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Wed, 10 Jun 2015 19:10:20 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Thu, 30 Apr 2015 15:28:01 +0100 |
paulson |
tidying some messy proofs
|
file |
diff |
annotate
|
| Tue, 28 Apr 2015 16:23:38 +0100 |
paulson |
New material about complex transcendental functions (especially Ln, Arg) and polynomials
|
file |
diff |
annotate
|
| Sat, 11 Apr 2015 11:56:40 +0100 |
paulson |
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
|
file |
diff |
annotate
|