| 2016-03-07 |
paulson |
complex_differentiable -> field_differentiable, etc. (making these theorems also available for type real)
|
file |
diff |
annotate
|
| 2016-03-07 |
paulson |
new material to Blochj's theorem, as well as supporting lemmas
|
file |
diff |
annotate
|
| 2016-02-23 |
nipkow |
resolved conflict
|
file |
diff |
annotate
|
| 2016-02-23 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| 2016-02-23 |
paulson |
New and revised material for (multivariate) analysis
|
file |
diff |
annotate
|
| 2016-01-11 |
paulson |
nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.
|
file |
diff |
annotate
|
| 2016-01-07 |
paulson |
revisions to limits and derivatives, plus new lemmas
|
file |
diff |
annotate
|
| 2016-01-04 |
eberlm |
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
|
file |
diff |
annotate
|
| 2015-12-30 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| 2015-12-29 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| 2015-12-28 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| 2015-12-27 |
wenzelm |
prefer symbols for "floor", "ceiling";
|
file |
diff |
annotate
|
| 2015-12-07 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| 2015-12-07 |
paulson |
Cauchy's integral formula for circles. Starting to fix eventually_mono.
|
file |
diff |
annotate
|
| 2015-12-01 |
paulson |
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
|
file |
diff |
annotate
|
| 2015-11-20 |
paulson |
Theory of homotopic paths (from HOL Light), plus comments and minor refinements
|
file |
diff |
annotate
|
| 2015-11-17 |
paulson |
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
|
file |
diff |
annotate
|
| 2015-11-13 |
paulson |
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
|
file |
diff |
annotate
|
| 2015-11-10 |
paulson |
Merge
|
file |
diff |
annotate
|
| 2015-11-10 |
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
|
| 2015-11-03 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
| 2015-10-29 |
eberlm |
added many small lemmas about setsum/setprod/powr/...
|
file |
diff |
annotate
|
| 2015-10-26 |
paulson |
new lemmas about topology, etc., for Cauchy integral formula
|
file |
diff |
annotate
|
| 2015-10-13 |
paulson |
new material on path_component_sets, inside, outside, etc. And more default simprules
|
file |
diff |
annotate
|
| 2015-08-31 |
wenzelm |
prefer symbols;
|
file |
diff |
annotate
|
| 2015-07-28 |
paulson |
the Cauchy integral theorem and related material
|
file |
diff |
annotate
|
| 2015-06-10 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| 2015-04-30 |
paulson |
tidying some messy proofs
|
file |
diff |
annotate
|
| 2015-04-28 |
paulson |
New material about complex transcendental functions (especially Ln, Arg) and polynomials
|
file |
diff |
annotate
|
| 2015-04-21 |
paulson |
New material, mostly about limits. Consolidation.
|
file |
diff |
annotate
|
| 2015-04-11 |
paulson |
Complex roots of unity. Better definition of ln for complex numbers. Used [code del] to stop code generation for powr.
|
file |
diff |
annotate
|
| 2015-04-11 |
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
|
| 2015-04-01 |
paulson |
HOL Light Libraries for complex Arctan, Arcsin, Arccos
|
file |
diff |
annotate
|
| 2015-03-31 |
paulson |
New material and binomial fix
|
file |
diff |
annotate
|
| 2015-03-19 |
paulson |
New material for complex sin, cos, tan, Ln, also some reorganisation
|
file |
diff |
annotate
|
| 2015-03-18 |
paulson |
new HOL Light material about exp, sin, cos
|
file |
diff |
annotate
|
| 2015-03-18 |
paulson |
new file for complex transcendental functions
|
file |
diff |
annotate
|