| 2011-09-13 |
bulwahn |
correcting NEWS
|
file |
diff |
annotate
|
| 2011-09-12 |
huffman |
NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| 2011-09-12 |
huffman |
remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def
|
file |
diff |
annotate
|
| 2011-09-12 |
huffman |
fix typos
|
file |
diff |
annotate
|
| 2011-09-12 |
huffman |
NEWS for euclidean_space class
|
file |
diff |
annotate
|
| 2011-09-12 |
hoelzl |
adding NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| 2011-09-12 |
bulwahn |
merged
|
file |
diff |
annotate
|
| 2011-09-12 |
bulwahn |
adding NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| 2011-09-12 |
bulwahn |
tuned some symbol that probably went there by some strange encoding issue
|
file |
diff |
annotate
|
| 2011-09-12 |
blanchet |
added my contributions to NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| 2011-09-12 |
nipkow |
NEWS fastsimp -> fastforce
|
file |
diff |
annotate
|
| 2011-09-11 |
huffman |
NEWS for Library/Product_Lattice.thy
|
file |
diff |
annotate
|
| 2011-09-08 |
krauss |
added syntactic classes for "inf" and "sup"
|
file |
diff |
annotate
|
| 2011-09-08 |
huffman |
merged
|
file |
diff |
annotate
|
| 2011-09-07 |
huffman |
remove duplicate lemma real_of_int_real_of_nat in favor of real_of_int_of_nat_eq
|
file |
diff |
annotate
|
| 2011-09-07 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2011-09-07 |
haftmann |
theory of saturated naturals contributed by Peter Gammie
|
file |
diff |
annotate
|
| 2011-09-07 |
wenzelm |
NEWS on IsabelleText font;
|
file |
diff |
annotate
|
| 2011-09-07 |
wenzelm |
some updates for release;
|
file |
diff |
annotate
|
| 2011-09-07 |
wenzelm |
some tuning for release;
|
file |
diff |
annotate
|
| 2011-09-07 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| 2011-09-06 |
wenzelm |
some Isabelle/jEdit NEWS;
|
file |
diff |
annotate
|
| 2011-09-06 |
huffman |
remove redundant lemma real_sum_squared_expand in favor of power2_sum
|
file |
diff |
annotate
|
| 2011-09-06 |
huffman |
remove redundant lemma LIMSEQ_Complex in favor of tendsto_Complex
|
file |
diff |
annotate
|
| 2011-09-04 |
huffman |
remove redundant lemmas expi_add and expi_zero
|
file |
diff |
annotate
|
| 2011-09-04 |
huffman |
remove redundant lemmas about LIMSEQ
|
file |
diff |
annotate
|
| 2011-09-03 |
huffman |
remove duplicate lemma finite_choice in favor of finite_set_choice
|
file |
diff |
annotate
|
| 2011-09-02 |
huffman |
remove redundant lemma reals_complete2 in favor of complete_real
|
file |
diff |
annotate
|
| 2011-09-02 |
huffman |
remove more duplicate lemmas
|
file |
diff |
annotate
|
| 2011-09-01 |
huffman |
simplify some proofs about uniform continuity, and add some new ones;
|
file |
diff |
annotate
|
| 2011-09-01 |
huffman |
modernize lemmas about 'continuous' and 'continuous_on';
|
file |
diff |
annotate
|
| 2011-08-28 |
huffman |
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
|
file |
diff |
annotate
|
| 2011-08-26 |
huffman |
NEWS entry for setsum_norm ~> norm_setsum
|
file |
diff |
annotate
|
| 2011-08-26 |
huffman |
replace some continuous_on lemmas with more general versions
|
file |
diff |
annotate
|
| 2011-08-25 |
huffman |
remove legacy theorem Lim_inner
|
file |
diff |
annotate
|
| 2011-08-25 |
huffman |
remove dot_lsum and dot_rsum in favor of inner_setsum_{left,right}
|
file |
diff |
annotate
|
| 2011-08-25 |
huffman |
rename subset_{interior,closure} to {interior,closure}_mono;
|
file |
diff |
annotate
|
| 2011-08-19 |
haftmann |
more concise definition for Inf, Sup on bool
|
file |
diff |
annotate
|
| 2011-08-18 |
huffman |
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
|
file |
diff |
annotate
|
| 2011-08-18 |
nipkow |
case_names NEWS
|
file |
diff |
annotate
|
| 2011-08-10 |
huffman |
more uniform naming scheme for finite cartesian product type and related theorems
|
file |
diff |
annotate
|
| 2011-08-09 |
haftmann |
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
|
file |
diff |
annotate
|
| 2011-08-09 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2011-08-08 |
haftmann |
dropped lemmas (Inf|Sup)_(singleton|binary)
|
file |
diff |
annotate
|
| 2011-08-09 |
huffman |
rename type 'a net to 'a filter, following standard mathematical terminology
|
file |
diff |
annotate
|
| 2011-08-04 |
haftmann |
NEWS
|
file |
diff |
annotate
|
| 2011-08-03 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| 2011-08-02 |
huffman |
Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
|
file |
diff |
annotate
|
| 2011-08-02 |
huffman |
NEWS: fix typo
|
file |
diff |
annotate
|
| 2011-08-02 |
krauss |
NEWS
|
file |
diff |
annotate
|
| 2011-07-25 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2011-07-24 |
haftmann |
more coherent structure in and across theories
|
file |
diff |
annotate
|
| 2011-07-25 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| 2011-07-20 |
haftmann |
class complete_linorder
|
file |
diff |
annotate
|
| 2011-07-18 |
haftmann |
avoid misunderstandable names
|
file |
diff |
annotate
|
| 2011-07-17 |
haftmann |
more on complement
|
file |
diff |
annotate
|
| 2011-07-17 |
haftmann |
more consistent theorem names
|
file |
diff |
annotate
|
| 2011-07-17 |
haftmann |
further generalization from sets to complete lattices
|
file |
diff |
annotate
|
| 2011-07-13 |
haftmann |
uniqueness lemmas for bot and top
|
file |
diff |
annotate
|
| 2011-07-13 |
haftmann |
adjusted to tightened specification of classes bot and top
|
file |
diff |
annotate
|