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 src/HOL/ex/Ballot
20150616, by hoelzl
add examples from Freek's top 100 theorems (thms 30, 73, 77)
20150612, by bulwahn
generalized geometric distribution
20150617, by hoelzl
added lemma
20150628, by nipkow
simplified termination criterion for euclidean algorithm (again)
20150627, by haftmann
tuned proof
20150627, by haftmann
rings follow immediately their corresponding semirings
20150627, by haftmann
tuned code setup
20150627, by haftmann
algebraic specification for set gcd
20150627, by haftmann
premises in 'show' are treated like 'assume';
20150627, by wenzelm
adapted to a9b71c82647b;
20150626, by wenzelm
merged
20150626, by wenzelm
isabelle update_cartouches;
20150626, by wenzelm
more symbols;
20150626, by wenzelm
tuned proofs;
20150626, by wenzelm
do not expose goal parameters;
20150626, by wenzelm
more symbols;
20150626, by wenzelm
more symbols;
20150626, by wenzelm
proper spacing, as for other syntax for these symbols;
20150626, by wenzelm
tuned whitespace;
20150626, by wenzelm
updated SystemOnTPTP URL
20150626, by blanchet
tuned proofs;
20150626, by wenzelm
merged
20150625, by wenzelm
implicit goal cases are legacy;
20150625, by wenzelm
tuned proofs;
20150625, by wenzelm
more heap  hoping for more stability of HOLProofs;
20150625, by wenzelm
added method "goals" for proper subgoal cases;
20150625, by wenzelm
tuned signature;
20150625, by wenzelm
tuned signature;
20150625, by wenzelm
tuned;
20150625, by wenzelm
tuned;
20150625, by wenzelm
tuned signature;
20150625, by wenzelm
streamlined definitions and primitive lemma of euclidean algorithm, including code generation
20150625, by haftmann
euclidean algorithm on polynomials
20150625, by haftmann
more theorems
20150625, by haftmann
generalized to definition from literature, which covers also polynomials
20150625, by haftmann
put E before (typically remote, hence less reliable) Vampire
20150625, by blanchet
tuned proofs  less digits;
20150624, by wenzelm
updated to scala2.11.7;
20150624, by wenzelm
clarified 'case' command;
20150624, by wenzelm
silence 'try'
20150624, by blanchet
Merge
20150623, by paulson
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
20150623, by paulson
tuned proofs;
20150623, by wenzelm
tuned proofs;
20150622, by wenzelm
merged
20150622, by wenzelm
tuned proofs;
20150622, by wenzelm
tuned proofs;
20150622, by wenzelm
tuned;
20150622, by wenzelm
support 'when' statement, which corresponds to 'presume';
20150622, by wenzelm
added method "sleep";
20150622, by wenzelm
tuned signature;
20150622, by wenzelm
tuned whitespace;
20150622, by wenzelm
clarified nesting of Isar goal structure;
20150622, by wenzelm
tuned;
20150622, by wenzelm
keep 'Pure.all' in goals when preplaying
20150622, by blanchet
use right context for preplay, to avoid errors in fact lookup
20150622, by blanchet
reverted some too aggressive TPTP interpreter changes
20150622, by blanchet
automatically build image
20150622, by blanchet
filter out more Poly/ML messages from (ad hoc) TPTP toools
20150622, by blanchet
less
more

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