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
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.
HOLProbability: more about probability, prepare for Markov processes in the AFP
20160930, by hoelzl
Merge
20161003, by paulson
new theorems including the theory FurtherTopology
20161003, by paulson
clarified magic values (see also java/io/BufferedInputStream.java);
20161003, by wenzelm
clarified stream operations;
20161003, by wenzelm
tuned signature;
20161003, by wenzelm
clarified modules;
20161003, by wenzelm
more general read_stream: return actual byte count;
20161003, by wenzelm
clarified modules;
20161002, by wenzelm
more operations;
20161002, by wenzelm
more operations;
20161002, by wenzelm
more formal Mercurial support (with the potential to upgrade to command server);
20161002, by wenzelm
tuned whitespace;
20161002, by wenzelm
added isabelle_java coldstart executable;
20161002, by wenzelm
updated according to 85c83757788c;
20161002, by wenzelm
eliminated hard tabs;
20161002, by wenzelm
updated headers;
20161002, by wenzelm
updated to sumatra_pdf3.1.2;
20161002, by wenzelm
updated to xzjava1.5;
20161002, by wenzelm
updated cygwin according to 9416333a17c2, still using old 1.7.351;
20161002, by wenzelm
tuned;
20161002, by wenzelm
just one option is enough  "isabelle jedit" java process may be prefixed directly in the shell;
20161002, by wenzelm
options for process policy, notably for multiprocessor machines;
20161001, by wenzelm
tuned;
20161001, by wenzelm
tuned messages  facilitate copypaste;
20161001, by wenzelm
merged
20161001, by wenzelm
tuned;
20161001, by wenzelm
tuned proofs;
20161001, by wenzelm
Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);
20161001, by wenzelm
clarified lfp/gfp statements and proofs;
20161001, by wenzelm
repair LaTeX
20161001, by Lars Hupel
misc tuning for release;
20161001, by wenzelm
added lemma;
20161001, by wenzelm
Trying out "subgoal", and no more [ ]
20160930, by paulson
HOLAnalysis: fix latex generation
20160930, by hoelzl
Probability: fix proof
20160930, by hoelzl
Library: fix name Product_plus to Product_Plus
20160930, by hoelzl
HOLAnalysis: move Product_Vector and Inner_Product from Library
20160930, by hoelzl
HOLAnalysis: move Continuum_Not_Denumerable from Library
20160930, by hoelzl
HOLAnalysis: move Library/Convex to Convex_Euclidean_Space
20160930, by hoelzl
HOLAnalysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
20160930, by hoelzl
new material on paths, etc. Also rationalisation
20160930, by paulson
Merged
20160930, by Manuel Eberl
Set_Permutations replaced by more general Multiset_Permutations
20160929, by eberlm
CONTRIBUTORS: new proof method "argo"
20160929, by boehmes
NEWS: new proof method "argo"
20160929, by boehmes
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
20160929, by boehmes
invoke argo as part of the tried automatic proof methods
20160929, by boehmes
new proof method "argo" for a combination of quantifierfree propositional logic with equality and linear real arithmetic
20160929, by boehmes
HOLAnalysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
20160929, by hoelzl
HOLAnalysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
20160929, by hoelzl
HOLAnalysis: move gauges and (tagged) divisions to its own theory file
20160929, by hoelzl
HOLAnalysis: add cover lemma ported by L. C. Paulson
20160928, by hoelzl
more new material
20160929, by paulson
Generalised the type of map_poly
20160929, by paulson
Merge
20160928, by paulson
new material connected with HOL Light measure theory, plus more rationalisation
20160928, by paulson
sequential (jobs = 1) makeall profile
20160928, by Lars Hupel
syntactic type class for operation mod named after mod;
20160926, by haftmann
dropped tautological pattern
20160926, by haftmann
less
more

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