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.
add simp rules for isCont
20110816, by huffman
updated keywords  old codegen is no longer in Pure;
20110816, by wenzelm
include HOLLibrary keywords for the sake of recdef;
20110816, by wenzelm
merged
20110816, by wenzelm
Multivariate_Analysis includes Determinants.thy, but doesn't import it by default
20110816, by huffman
get Multivariate_Analysis/Determinants.thy compiled and working again
20110816, by huffman
get Library/Permutations.thy compiled and working again
20110816, by huffman
workaround for Cygwin, to make it work in the important special case without extra files;
20110816, by wenzelm
more robust Thy_Header.base_name, with minimal assumptions about path syntax;
20110816, by wenzelm
tuned message;
20110816, by wenzelm
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
less
more

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