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.
simplified basic termination proof
20130308, by nipkow
some simp rules for fset
20130308, by traytel
avoid Infinity which confuses JFreeChart histogram;
20130307, by wenzelm
tuned proofs  more structure, less warnings;
20130307, by wenzelm
tuned signature  prefer terminology of Scala and Axiom;
20130307, by wenzelm
better message (typeunsoundnesses are becoming rare, usually the issue is elsewhere, e.g. in the TSTP proof parser)
20130307, by blanchet
avoid using Arith_Data.dest_sum in extendednat simprocs (it treats 'x  y' as 'x +  y', which is not valid for enat)
20130306, by huffman
netlimit is abbreviation for Lim
20130306, by hoelzl
tuned proofs
20130306, by hoelzl
changed has_derivative_intros into a named theorems collection
20130306, by hoelzl
changed continuous_on_intros into a named theorems collection
20130306, by hoelzl
changed continuous_intros into a named theorems collection
20130306, by hoelzl
add tendsto_eq_intros: they add an additional rewriting step at the rhs of >
20130306, by hoelzl
major redesign: order instead of preorder, new definition of intervals as quotients
20130306, by nipkow
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
less
more

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