| 2016-05-23 |
paulson |
deleted needless comment
|
file |
diff |
annotate
|
| 2016-05-23 |
paulson |
Lots of new material for multivariate analysis
|
file |
diff |
annotate
|
| 2016-05-13 |
wenzelm |
eliminated use of empty "assms";
|
file |
diff |
annotate
|
| 2016-04-25 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
| 2016-04-18 |
paulson |
numerous theorems about affine hulls, hyperplanes, etc.
|
file |
diff |
annotate
|
| 2016-04-11 |
paulson |
lots of new theorems for multivariate analysis
|
file |
diff |
annotate
|
| 2016-04-04 |
paulson |
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
|
file |
diff |
annotate
|
| 2016-03-16 |
paulson |
Contractible sets. Also removal of obsolete theorems and refactoring
|
file |
diff |
annotate
|
| 2016-03-14 |
paulson |
New results about paths, segments, etc. The notion of simply_connected.
|
file |
diff |
annotate
|
| 2016-03-14 |
paulson |
Refactoring (moving theorems into better locations), plus a bit of new material
|
file |
diff |
annotate
|
| 2016-03-07 |
paulson |
new material to Blochj's theorem, as well as supporting lemmas
|
file |
diff |
annotate
|
| 2016-02-24 |
paulson |
Merge
|
file |
diff |
annotate
|
| 2016-02-24 |
paulson |
Substantial new material for multivariate analysis. Also removal of some duplicates.
|
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-07 |
paulson |
revisions to limits and derivatives, plus new lemmas
|
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-23 |
paulson |
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
|
file |
diff |
annotate
|
| 2015-11-20 |
paulson |
Theory of homotopic paths (from HOL Light), plus comments and minor refinements
|
file |
diff |
annotate
|
| 2015-11-18 |
paulson |
New theorems mostly from Peter Gammie
|
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-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-09-21 |
paulson |
new lemmas and movement of lemmas into place
|
file |
diff |
annotate
|
| 2015-08-19 |
paulson |
New material and fixes related to the forthcoming Stone-Weierstrass development
|
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-05-26 |
paulson |
New material about paths, and some lemmas
|
file |
diff |
annotate
|
| 2015-02-19 |
haftmann |
establish unique preferred fact names
|
file |
diff |
annotate
|
| 2014-11-02 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| 2014-04-02 |
hoelzl |
extend continuous_intros; remove continuous_on_intros and isCont_intros
|
file |
diff |
annotate
|
| 2014-03-18 |
immler |
use cbox to relax class constraints
|
file |
diff |
annotate
|
| 2013-09-14 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| 2013-09-12 |
huffman |
removed outdated comments
|
file |
diff |
annotate
|
| 2013-03-22 |
hoelzl |
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
|
file |
diff |
annotate
|
| 2013-03-22 |
hoelzl |
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
|
file |
diff |
annotate
|
| 2013-01-17 |
hoelzl |
generalize compact_path_image to topological_space
|
file |
diff |
annotate
|
| 2013-01-14 |
hoelzl |
differentiate (cover) compactness and sequential compactness
|
file |
diff |
annotate
|
| 2012-12-14 |
hoelzl |
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
|
file |
diff |
annotate
|
| 2012-09-28 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| 2012-09-28 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| 2012-06-25 |
wenzelm |
tuned proofs -- prefer direct "rotated" instead of old-style COMP;
|
file |
diff |
annotate
|
| 2011-09-01 |
huffman |
modernize lemmas about 'continuous' and 'continuous_on';
|
file |
diff |
annotate
|
| 2011-08-26 |
huffman |
replace some continuous_on lemmas with more general versions
|
file |
diff |
annotate
|
| 2011-08-12 |
huffman |
make Multivariate_Analysis work with separate set type
|
file |
diff |
annotate
|
| 2011-03-13 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| 2010-09-13 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| 2010-07-01 |
huffman |
convert theorem path_connected_sphere to euclidean_space class
|
file |
diff |
annotate
|
| 2010-06-21 |
hoelzl |
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
|
file |
diff |
annotate
|
| 2010-04-28 |
huffman |
move path-related stuff into new theory file
|
file |
diff |
annotate
|