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.
Determinants.thy: avoid using mem_def/Collect_def
20110817, by huffman
Wfrec.thy: respect set/pred distinction
20110817, by huffman
follow updates of Isabelle/Pure;
20110818, by wenzelm
merged
20110817, by wenzelm
IsaMakefile: target HOLCFLibrary now compiles HOL/HOLCF/Library instead of HOL/Library
20110817, by huffman
merged
20110817, by huffman
Lim.thy: generalize and simplify proofs of LIM/LIMSEQ theorems
20110817, by huffman
add lemma tendsto_compose_eventually; use it to shorten some proofs
20110817, by huffman
Topology_Euclidean_Space.thy: simplify some proofs
20110817, by huffman
add lemma metric_tendsto_imp_tendsto
20110817, by huffman
simplify proofs of lemmas open_interval, closed_interval
20110817, by huffman
identify parallel exceptions where they emerge first  to achieve unique results within evaluation graph;
20110817, by wenzelm
clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;
20110817, by wenzelm
more systematic handling of parallel exceptions;
20110817, by wenzelm
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
less
more

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