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.
tuned signature;
20110817, by wenzelm
merged
20110817, by haftmann
merged
20110817, by haftmann
merged
20110817, by haftmann
avoid Collect_def in proof
20110816, by haftmann
modernized signature of Term.absfree/absdummy;
20110817, by wenzelm
improved default context for ML toplevel prettyprinting;
20110817, by wenzelm
less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
20110817, by wenzelm
some convenience actions/shortcuts for control symbols;
20110817, by wenzelm
export Function_Fun.fun_config for user convenience;
20110817, by wenzelm
moved theory Nested_Environment to HOLUnix (a bit too specific for HOLLibrary);
20110817, by wenzelm
distinguish THF syntax with and without choice (Satallax vs. LEOII)
20110817, by blanchet
merged
20110816, by huffman
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
less
more

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