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
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScriptenabled browsers.
tuned proof of Edelstein fixed point theorem (use continuity of dist and attains_sup)
20130305, by hoelzl
tuned proofs (used continuity of infdist, dist and continuous_attains_sup)
20130305, by hoelzl
generalized continuous/compact_attains_inf/sup from real to linorder_topology
20130305, by hoelzl
continuity of pair operations
20130305, by hoelzl
use generate_topology for second countable topologies, does not require intersection stable basis
20130305, by hoelzl
generalized isGlb_unique
20130305, by hoelzl
complete_linorder is also a complete_distrib_lattice
20130305, by hoelzl
move Liminf / Limsup lemmas on complete_lattices to its own file
20130305, by hoelzl
merged
20130305, by nipkow
New theory of infinityextended types; should replace Extended_xyz eventually
20130305, by nipkow
Avoid ML warning about unreferenced identifier.
20130305, by webertj
polymorphic SPASS is also SPASS
20130305, by blanchet
allow more general coercion maps; tuned;
20130305, by traytel
more lemmas about intervals
20130305, by nipkow
merged
20130304, by wenzelm
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
20130304, by wenzelm
join all proofs before scheduling present phase (ordered according to weight);
20130304, by wenzelm
more explicit datatype result;
20130304, by wenzelm
split dense into inner_dense_order and no_top/no_bot
20130220, by hoelzl
move auxiliary lemmas from Library/Extended_Reals to HOL image
20130220, by hoelzl
tuned (extend datatype to inline option)
20130304, by traytel
prefer more systematic Future.flat;
20130303, by wenzelm
more uniform Future.map: always internalize failure;
20130303, by wenzelm
uniform treatment of global/local proofs;
20130303, by wenzelm
tuned;
20130303, by wenzelm
clarified Toplevel.element_result wrt. Toplevel.is_ignored;
20130303, by wenzelm
more Thy_Syntax.element operations;
20130303, by wenzelm
coercioninvariant arguments at work
20130301, by traytel
constants with coercioninvariant arguments (possibility to disable/reenable
20130301, by traytel
simplified Proof.future_proof;
20130228, by wenzelm
less
more

(0)
30000
10000
3000
1000
300
100
50
30
+30
+50
+100
+300
+1000
+3000
+10000
tip