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.
remove extraneous subsection heading
20110815, by huffman
generalized lemma closed_Collect_eq
20110815, by huffman
remove duplicate lemma disjoint_iff
20110815, by huffman
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
20110815, by huffman
add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq;
20110815, by huffman
generalize lemma continuous_uniform_limit to class metric_space
20110815, by huffman
remove duplicate lemmas eventually_conjI, eventually_and, eventually_false
20110815, by huffman
Topology_Euclidean_Space.thy: organize section headings
20110815, by huffman
simplify some proofs
20110815, by huffman
generalize lemma convergent_subseq_convergent
20110814, by huffman
localeize some definitions, so perfect_space and heine_borel can inherit from the proper superclasses
20110814, by huffman
localeize some constant definitions, so complete_space can inherit from metric_space
20110814, by huffman
generalize constant 'lim' and limit uniqueness theorems to class t2_space
20110814, by huffman
Quotient Package: make quotient_type work with separate set type
20110816, by Cezary Kaliszyk
updated README;
20110815, by wenzelm
touch descendants of edited nodes;
20110815, by wenzelm
parellel scheduling of node edits and execution;
20110815, by wenzelm
tuned error message;
20110815, by wenzelm
retrieve imports from document state, with fallback on theory loader for preloaded theories;
20110815, by wenzelm
explicit check of finished evaluation;
20110815, by wenzelm
refined Document.edit: less stateful update via Graph.schedule;
20110815, by wenzelm
simplified exec: eliminated unused status flag;
20110815, by wenzelm
consistently use variable name 'F' for filters
20110814, by huffman
generalize lemmas about LIM and LIMSEQ to tendsto
20110814, by huffman
HOLNominalExamples: respect distinction between sets and functions
20110813, by huffman
less verbosity in batch mode  spam reduction and notable performance improvement;
20110813, by wenzelm
merged
20110813, by wenzelm
HOLHahn_Banach: use Set_Algebras library
20110813, by huffman
ex/Quickcheck_Examples.thy: respect distinction between sets and functions
20110813, by huffman
clarified Toplevel.end_theory;
20110813, by wenzelm
less
more

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