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
+30000
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.
more robust treatment of node dependencies in incremental edits;
20110816, by wenzelm
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
20110816, by wenzelm
omit MiscUtilities.resolveSymlinks for now  odd effects on caseinsensible filesystem;
20110816, by wenzelm
merged
20110815, by huffman
generalize lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq to class topological_space
20110815, by huffman
add lemma tendsto_compose
20110815, by huffman
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
simplified Toplevel.init_theory: discontinued special name argument;
20110813, by wenzelm
simplified Toplevel.init_theory: discontinued special master argument;
20110813, by wenzelm
provide node header via Scala layer;
20110813, by wenzelm
reduced verbosity;
20110813, by wenzelm
tuned signature;
20110813, by wenzelm
clarified node header  exclude master_dir;
20110813, by wenzelm
tuned;
20110813, by wenzelm
maintain node header;
20110813, by wenzelm
removed unused lemma; removed oldstyle ;
20110813, by kleing
point isateststatistics to the right afp log files
20110813, by kleing
IMP/Util distinguishes between sets and functions again; imported only where used.
20110813, by kleing
remove redundant lemma setsum_norm in favor of norm_setsum;
20110812, by huffman
merged
20110812, by huffman
make more HOL theories work with separate set type
20110812, by huffman
immediate fork of initial workers  avoid 5 ticks (250ms) for adaptive scheme (a07558eb5029);
20110813, by wenzelm
merged
20110812, by wenzelm
merged
20110812, by huffman
make Multivariate_Analysis work with separate set type
20110812, by huffman
make HOLCF work with separate set type
20110812, by huffman
merged
20110812, by huffman
avoid duplicate rule warnings
20110811, by huffman
modify euclidean_space class to include basis set
20110811, by huffman
remove lemma stupid_ext
20110811, by huffman
documented extended version of case_names attribute
20110812, by nipkow
less
more

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