Mercurial
Mercurial
>
repos
>
testboard
/ 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.
tuned;
20130120, by wenzelm
accomodate scala2.9.2;
20130120, by wenzelm
afford parallel proof terms;
20130119, by wenzelm
always close derivation at the bottom of forked proofs (despite increased nondeterminism of proof terms)  improve parallel performance by avoiding dynamic dependency within large Isar proofs, e.g. Slicing/JinjaVM/SemanticsWF.thy in AFP/bf9b14cbc707;
20130119, by wenzelm
simplified proofs
20130119, by nipkow
tuning
20130119, by blanchet
misc cleanup;
20130119, by wenzelm
tuned signature;
20130119, by wenzelm
use inlined session name as title for charts;
20130118, by wenzelm
tuned signature;
20130118, by wenzelm
charts for future task runtime statistics;
20130118, by wenzelm
merged
20130118, by wenzelm
more uniform permissions;
20130118, by wenzelm
more generous C stack size as in Linux and Mac OS X, to reduce chance of Cygwinspecific crashes;
20130118, by wenzelm
tuned proof  much faster;
20130118, by wenzelm
more systematic task statistics;
20130118, by wenzelm
added "tasks_proof" statistics, via slighly odd global reference Future.forked_proofs (NB: Future.report_status is intertwined with scheduler thread);
20130118, by wenzelm
generalized diameter from real_normed_vector to metric_space
20130118, by hoelzl
tuned proof
20130118, by hoelzl
tune prove compact_eq_totally_bounded
20130118, by hoelzl
generalized theorem edelstein_fix to class metric_space
20130117, by huffman
tuning
20130118, by blanchet
pass correct index to "Sign.typ_unify"  this is important to avoid what appears to be an infinite loop in the unifier
20130118, by blanchet
optimization  evaluate conversion to table only once
20130118, by blanchet
MeSh prover generation
20130117, by blanchet
use correct weights in MeSh driver
20130117, by blanchet
use precomputed MaSh/MePo data whenever available
20130117, by blanchet
merged
20130117, by wenzelm
merged
20130117, by wenzelm
copy CygwinLatexSetup.bat;
20130117, by wenzelm
more formal CygwinLatexSetup (excluding bulky texlivecollectionfontsextra, which would be required for eulervm.sty);
20130117, by wenzelm
updated to cygwin20130117;
20130117, by wenzelm
proper permissions;
20130117, by wenzelm
tuned;
20130117, by wenzelm
updated to jdk7u11;
20130117, by wenzelm
simplify proof of compact_imp_bounded
20130117, by huffman
added step to skip some queries
20130117, by blanchet
provide a means to skip a method
20130117, by blanchet
evaluate more cases (cf. paper)
20130117, by blanchet
updated MaSh
20130117, by blanchet
make SPASS more configurable, for experiments
20130117, by blanchet
generalize more topology lemmas
20130115, by huffman
generalize topology lemmas; simplify proofs
20130115, by huffman
merged
20130117, by wenzelm
tuned signature (again)  keep Properties more generic;
20130117, by wenzelm
tuned proofs;
20130117, by wenzelm
simplified prove of compact_imp_bounded
20130117, by hoelzl
use accumulation point characterization (avoids t1_space restriction for equivalence of countable and sequential compactness); remove heine_borel_lemma
20130117, by hoelzl
move auxiliary lemma to top
20130117, by hoelzl
add countable compacteness; replace finite_range_imp_infinite_repeats by pigeonhole_infinite
20130117, by hoelzl
group compactnesseqseqcompactness lemmas together
20130117, by hoelzl
replace convergent_imp_cauchy by LIMSEQ_imp_Cauchy
20130117, by hoelzl
tuned
20130117, by hoelzl
removed subseq_bigger (replaced by seq_suble)
20130117, by hoelzl
countablility of finite subsets and rational numbers
20130117, by hoelzl
generalize compact_path_image to topological_space
20130117, by hoelzl
regenerated components.sha1;
20130117, by wenzelm
merged
20130117, by wenzelm
more systemindependent order of components.sha1 to keep changes monotonic;
20130117, by wenzelm
clarified Future.error_msg: slightly more robust id check, actually suppress displaced messages;
20130117, by wenzelm
less
more

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