Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-50
-30
+30
+50
+100
+300
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
add tendsto_eq_intros: they add an additional rewriting step at the rhs of --->
2013-03-06, by hoelzl
major redesign: order instead of preorder, new definition of intervals as quotients
2013-03-06, by nipkow
added lemma
2013-03-06, by nipkow
extended numerals
2013-03-06, by nipkow
merged
2013-03-05, by wenzelm
merged
2013-03-05, by wenzelm
removed unused Future.flat, while leaving its influence of Future.map (see bcd6b1aa4db5);
2013-03-05, by wenzelm
extended stream library a little more
2013-03-05, by traytel
extended stream library
2013-03-05, by traytel
generalized lemmas in Extended_Real_Limits
2013-03-05, by hoelzl
eventually nhds represented using sequentially
2013-03-05, by hoelzl
generalized compact_Times to topological_space
2013-03-05, by hoelzl
move lemma Inf to usage point
2013-03-05, by hoelzl
tuned proof of Edelstein fixed point theorem (use continuity of dist and attains_sup)
2013-03-05, by hoelzl
tuned proofs (used continuity of infdist, dist and continuous_attains_sup)
2013-03-05, by hoelzl
generalized continuous/compact_attains_inf/sup from real to linorder_topology
2013-03-05, by hoelzl
continuity of pair operations
2013-03-05, by hoelzl
use generate_topology for second countable topologies, does not require intersection stable basis
2013-03-05, by hoelzl
generalized isGlb_unique
2013-03-05, by hoelzl
complete_linorder is also a complete_distrib_lattice
2013-03-05, by hoelzl
move Liminf / Limsup lemmas on complete_lattices to its own file
2013-03-05, by hoelzl
merged
2013-03-05, by nipkow
New theory of infinity-extended types; should replace Extended_xyz eventually
2013-03-05, by nipkow
Avoid ML warning about unreferenced identifier.
2013-03-05, by webertj
polymorphic SPASS is also SPASS
2013-03-05, by blanchet
allow more general coercion maps; tuned;
2013-03-05, by traytel
more lemmas about intervals
2013-03-05, by nipkow
merged
2013-03-04, by wenzelm
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
2013-03-04, by wenzelm
join all proofs before scheduling present phase (ordered according to weight);
2013-03-04, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-50
-30
+30
+50
+100
+300
+1000
+3000
+10000
+30000
tip