Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
30000
10000
3000
1000
300
100
50
30
+30
+50
+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.
updated latex dependencies (cf. 7d88ebdce380);
20101203, by wenzelm
tuned README;
20101203, by wenzelm
isabellesym.sty: eliminated dependency on latin1, to allow documents using utf8 instead;
20101202, by wenzelm
proper theory name (cf. e84f82418e09);
20101202, by wenzelm
merged;
20101202, by wenzelm
merged
20101202, by huffman
tuned cpodef code
20101201, by huffman
reformulate lemma preorder.ex_ideal, and use it for typedefs
20101201, by huffman
Prove rel_interior_convex_hull_union (by Grechuck Bogdan).
20101202, by hoelzl
merged
20101202, by haftmann
adapted expected value to more idiomatic numeral representation
20101202, by haftmann
corrected representation for code_numeral numerals
20101202, by haftmann
separate term_of function for integers  more canonical representation of negative integers
20101202, by haftmann
merged
20101202, by hoelzl
Use coercions in Approximation (by Dmitriy Traytel).
20101202, by hoelzl
more antiquotations;
20101202, by wenzelm
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
20101202, by wenzelm
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
20101202, by wenzelm
merged
20101202, by wenzelm
merged
20101202, by hoelzl
generalized simple_functionD
20101202, by hoelzl
Moved theorems to appropriate place.
20101202, by hoelzl
Shorter definition for positive_integral.
20101202, by hoelzl
Move SUP_commute, SUP_less_iff to HOL image;
20101202, by hoelzl
Generalized simple_functionD and less_SUP_iff.
20101201, by hoelzl
Tuned setup for borel_measurable with min, max and psuminf.
20101201, by hoelzl
Replace algebra_eqI by algebra.equality;
20101201, by hoelzl
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one  this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
20101202, by blanchet
merged
20101202, by wenzelm
coercions
20101202, by nipkow
less
more

(0)
30000
10000
3000
1000
300
100
50
30
+30
+50
+100
+300
+1000
+3000
+10000
+30000
tip