| 2016-05-23 |
paulson |
Lots of new material for multivariate analysis
|
file |
diff |
annotate
|
| 2016-05-09 |
paulson |
lemmas about dimension, hyperplanes, span, etc.
|
file |
diff |
annotate
|
| 2016-05-09 |
paulson |
renamings and refinements
|
file |
diff |
annotate
|
| 2016-04-22 |
hoelzl |
Linear_Algebra: generalize linear_surjective_right/injective_left_inverse to real vector spaces
|
file |
diff |
annotate
|
| 2016-04-22 |
hoelzl |
Linear_Algebra: generalize linear_independent_extend to all real vector spaces
|
file |
diff |
annotate
|
| 2016-04-22 |
hoelzl |
Linear_Algebra: alternative representation of linear combination
|
file |
diff |
annotate
|
| 2016-04-22 |
hoelzl |
Linear_Algebra: move abstract concepts to front
|
file |
diff |
annotate
|
| 2016-04-18 |
paulson |
new theorems about convex hulls, etc.; also, renamed some theorems
|
file |
diff |
annotate
|
| 2016-04-11 |
paulson |
lots of new theorems for multivariate analysis
|
file |
diff |
annotate
|
| 2016-03-15 |
paulson |
rationalisation of theorem names esp about "real Archimedian" etc.
|
file |
diff |
annotate
|
| 2016-02-24 |
paulson |
Substantial new material for multivariate analysis. Also removal of some duplicates.
|
file |
diff |
annotate
|
| 2016-02-17 |
haftmann |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
file |
diff |
annotate
|
| 2015-12-30 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| 2015-12-22 |
immler |
theory for type of bounded linear functions; differentiation under the integral sign
|
file |
diff |
annotate
|
| 2015-12-07 |
wenzelm |
isabelle update_cartouches -c -t;
|
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-10-27 |
paulson |
Cauchy's integral formula, required lemmas, and a bit of reorganisation
|
file |
diff |
annotate
|
| 2015-10-26 |
paulson |
new lemmas about topology, etc., for Cauchy integral formula
|
file |
diff |
annotate
|
| 2015-10-02 |
paulson |
New theorems about connected sets. And pairwise moved to Set.thy.
|
file |
diff |
annotate
|
| 2015-09-30 |
paulson |
real_of_nat_Suc is now a simprule
|
file |
diff |
annotate
|
| 2015-09-21 |
wenzelm |
isabelle update_cartouches;
|
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 |
tweaks. Got rid of a really slow step
|
file |
diff |
annotate
|
| 2015-07-27 |
paulson |
New material for Cauchy's integral theorem
|
file |
diff |
annotate
|
| 2015-07-20 |
paulson |
new material for multivariate analysis, etc.
|
file |
diff |
annotate
|
| 2015-06-10 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| 2015-05-28 |
paulson |
Convex hulls: theorems about interior, etc. And a few simple lemmas.
|
file |
diff |
annotate
|
| 2015-05-26 |
paulson |
New material about paths, and some lemmas
|
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-03-31 |
paulson |
rationalised and generalised some theorems concerning abs and x^2.
|
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-07-05 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
file |
diff |
annotate
|
| 2014-07-04 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| 2014-06-28 |
haftmann |
fact consolidation
|
file |
diff |
annotate
|
| 2014-04-11 |
nipkow |
made mult_nonneg_nonneg a simp rule
|
file |
diff |
annotate
|
| 2014-04-09 |
hoelzl |
field_simps: better support for negation and division, and power
|
file |
diff |
annotate
|
| 2014-04-09 |
hoelzl |
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
|
file |
diff |
annotate
|
| 2014-04-06 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| 2014-04-03 |
paulson |
removing simprule status for divide_minus_left and divide_minus_right
|
file |
diff |
annotate
|
| 2014-03-18 |
huffman |
remove unnecessary finiteness assumptions from lemmas about setsum
|
file |
diff |
annotate
|
| 2014-03-16 |
haftmann |
normalising simp rules for compound operators
|
file |
diff |
annotate
|
| 2014-03-04 |
huffman |
tuned proof
|
file |
diff |
annotate
|
| 2014-02-27 |
paulson |
A bit of tidying up
|
file |
diff |
annotate
|
| 2014-01-25 |
wenzelm |
tuned proof;
|
file |
diff |
annotate
|
| 2013-12-16 |
immler |
summarized notions related to ordered_euclidean_space and intervals in separate theory
|
file |
diff |
annotate
|
| 2013-12-16 |
immler |
introduced ordered real vector spaces
|
file |
diff |
annotate
|
| 2013-12-16 |
immler |
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
|
file |
diff |
annotate
|
| 2013-12-09 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| 2013-11-19 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| 2013-11-12 |
hoelzl |
add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image
|
file |
diff |
annotate
|
| 2013-11-01 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
| 2013-09-26 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| 2013-09-26 |
huffman |
moved lemma
|
file |
diff |
annotate
|
| 2013-09-24 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| 2013-09-18 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| 2013-09-13 |
huffman |
make 'linear' into a sublocale of 'bounded_linear';
|
file |
diff |
annotate
|
| 2013-09-12 |
huffman |
new lemmas
|
file |
diff |
annotate
|
| 2013-09-12 |
huffman |
prefer theorem name over 'long_thm_list(n)'
|
file |
diff |
annotate
|