Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
30000
10000
3000
1000
300
100
60
+60
+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.
added lemma
20130306, by nipkow
extended numerals
20130306, by nipkow
merged
20130305, by wenzelm
merged
20130305, by wenzelm
removed unused Future.flat, while leaving its influence of Future.map (see bcd6b1aa4db5);
20130305, by wenzelm
extended stream library a little more
20130305, by traytel
extended stream library
20130305, by traytel
generalized lemmas in Extended_Real_Limits
20130305, by hoelzl
eventually nhds represented using sequentially
20130305, by hoelzl
generalized compact_Times to topological_space
20130305, by hoelzl
move lemma Inf to usage point
20130305, by hoelzl
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
provide explicit dummy names (cf. dfe469293eb4);
20130228, by wenzelm
discontinued empty name bindings in 'axiomatization';
20130228, by wenzelm
provide common HOLogic.conj_conv and HOLogic.eq_conv;
20130228, by wenzelm
just one HOLogic.Trueprop_conv, with regular exception CTERM;
20130228, by wenzelm
discontinued obsolete 'axioms' command;
20130228, by wenzelm
more robust build error handling, e.g. missing outer syntax commands;
20130228, by wenzelm
eliminated legacy 'axioms';
20130228, by wenzelm
eliminated legacy 'axioms';
20130228, by wenzelm
eliminated legacy 'axioms';
20130228, by wenzelm
eliminated legacy 'axioms';
20130228, by wenzelm
eliminated legacy 'axioms';
20130228, by wenzelm
eliminated legacy 'axioms';
20130228, by wenzelm
eliminated legacy 'axioms';
20130228, by wenzelm
marginalized historic strip_tac;
20130228, by wenzelm
tuned proof;
20130228, by wenzelm
tuned whitespace and indentation;
20130228, by wenzelm
simplified imports;
20130228, by wenzelm
load timings in parallel for improved performance;
20130228, by wenzelm
proper place for cancel_div_mod.ML (see also ee729dbd1b7f and ec7f10155389);
20130228, by wenzelm
less
more

(0)
30000
10000
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
tip