| 2014-03-25 |
hoelzl |
cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
|
file |
diff |
annotate
|
| 2014-03-18 |
huffman |
remove unnecessary finiteness assumptions from lemmas about setsum
|
file |
diff |
annotate
|
| 2014-03-18 |
hoelzl |
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
|
file |
diff |
annotate
|
| 2014-03-18 |
immler |
removed dependencies on theory Ordered_Euclidean_Space
|
file |
diff |
annotate
|
| 2014-03-18 |
immler |
use cbox to relax class constraints
|
file |
diff |
annotate
|
| 2014-02-16 |
wenzelm |
tuned proofs;
|
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-16 |
immler |
prefer box over greaterThanLessThan on euclidean_space
|
file |
diff |
annotate
|
| 2013-11-19 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| 2013-11-01 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
| 2013-09-13 |
huffman |
make 'linear' into a sublocale of 'bounded_linear';
|
file |
diff |
annotate
|
| 2013-09-12 |
huffman |
prefer theorem name over 'long_thm_list(n)'
|
file |
diff |
annotate
|
| 2013-09-12 |
huffman |
removed outdated comments
|
file |
diff |
annotate
|
| 2013-04-18 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| 2013-04-09 |
hoelzl |
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
|
file |
diff |
annotate
|
| 2013-03-23 |
haftmann |
fundamental revision of big operators on sets
|
file |
diff |
annotate
|
| 2013-01-31 |
hoelzl |
simplify heine_borel type class
|
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-10-19 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| 2012-09-28 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| 2012-09-07 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| 2012-03-25 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| 2011-09-20 |
huffman |
add lemmas within_empty and tendsto_bot;
|
file |
diff |
annotate
|
| 2011-09-12 |
huffman |
remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def
|
file |
diff |
annotate
|
| 2011-09-01 |
huffman |
modernize lemmas about 'continuous' and 'continuous_on';
|
file |
diff |
annotate
|
| 2011-08-29 |
huffman |
move class perfect_space into RealVector.thy;
|
file |
diff |
annotate
|
| 2011-08-25 |
huffman |
rename subset_{interior,closure} to {interior,closure}_mono;
|
file |
diff |
annotate
|
| 2011-08-25 |
huffman |
simplify many proofs about subspace and span;
|
file |
diff |
annotate
|
| 2011-08-23 |
huffman |
declare euclidean_simps [simp] at the point they are proved;
|
file |
diff |
annotate
|
| 2011-08-22 |
huffman |
legacy theorem names
|
file |
diff |
annotate
|
| 2011-08-21 |
huffman |
section -> subsection
|
file |
diff |
annotate
|
| 2011-08-18 |
huffman |
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
|
file |
diff |
annotate
|
| 2011-08-16 |
huffman |
add simp rules for isCont
|
file |
diff |
annotate
|
| 2011-08-16 |
huffman |
generalize lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq to class topological_space
|
file |
diff |
annotate
|
| 2011-08-15 |
huffman |
add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq;
|
file |
diff |
annotate
|
| 2011-08-15 |
huffman |
remove duplicate lemmas eventually_conjI, eventually_and, eventually_false
|
file |
diff |
annotate
|
| 2011-08-12 |
huffman |
make Multivariate_Analysis work with separate set type
|
file |
diff |
annotate
|
| 2011-08-11 |
huffman |
avoid duplicate rule warnings
|
file |
diff |
annotate
|
| 2011-08-11 |
huffman |
modify euclidean_space class to include basis set
|
file |
diff |
annotate
|
| 2011-08-11 |
huffman |
remove lemma stupid_ext
|
file |
diff |
annotate
|
| 2011-08-10 |
huffman |
remove several redundant and unused theorems about derivatives
|
file |
diff |
annotate
|
| 2011-08-10 |
huffman |
more uniform naming scheme for finite cartesian product type and related theorems
|
file |
diff |
annotate
|
| 2011-08-10 |
huffman |
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
|
file |
diff |
annotate
|
| 2011-08-10 |
huffman |
simplified definition of class euclidean_space;
|
file |
diff |
annotate
|
| 2011-08-08 |
huffman |
fix perfect_space instance proof for finite cartesian product (cf. 5b970711fb39)
|
file |
diff |
annotate
|
| 2011-07-28 |
hoelzl |
simplified definition of vector (also removed Cartesian_Euclidean_Space.from_nat which collides with Countable.from_nat)
|
file |
diff |
annotate
|
| 2011-05-15 |
wenzelm |
simplified/unified method_setup/attribute_setup;
|
file |
diff |
annotate
|
| 2010-11-28 |
nipkow |
gave more standard finite set rules simp and intro attribute
|
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-09-07 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| 2010-08-23 |
hoelzl |
Rewrite the Probability theory.
|
file |
diff |
annotate
|
| 2010-08-20 |
haftmann |
more concise characterization of of_nat operation and class semiring_char_0
|
file |
diff |
annotate
|
| 2010-07-01 |
haftmann |
"prod" and "sum" replace "*" and "+" respectively
|
file |
diff |
annotate
|
| 2010-07-01 |
hoelzl |
Add theory for indicator function.
|
file |
diff |
annotate
|
| 2010-07-01 |
hoelzl |
Instantiate product type as euclidean space.
|
file |
diff |
annotate
|
| 2010-06-23 |
hoelzl |
Make latex happy
|
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
|