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
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.
no censorship of "view.fracFontMetrics", although it often degrades rendering quality;
20130323, by wenzelm
retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
20130323, by wenzelm
apply small result immediately, to avoid visible delay of text update after window move;
20130323, by wenzelm
structural equality for Command.Results;
20130323, by wenzelm
allow fractional pretty margin  avoid premature rounding;
20130323, by wenzelm
more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments)  NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
20130323, by wenzelm
tuned;
20130323, by wenzelm
spelling
20130323, by haftmann
fundamental revision of big operators on sets
20130323, by haftmann
tuned proof
20130323, by haftmann
locales for abstract orders
20130323, by haftmann
merged
20130323, by krauss
added rudimentary induction rule for partial_function (heap)
20130322, by krauss
allow induction predicates with arbitrary arity (not just binary)
20130322, by krauss
modernized definition of root: use the_inv, handle positive and negative case uniformly, and 0th root is constant 0
20130322, by hoelzl
arcsin and arccos are continuous on {0 .. 1} (including the endpoints)
20130322, by hoelzl
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
20130322, by hoelzl
move connected to HOL image; used to show intermediate value theorem
20130322, by hoelzl
move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets
20130322, by hoelzl
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
20130322, by hoelzl
clean up lemma_nest_unique and renamed to nested_sequence_unique
20130322, by hoelzl
simplify proof of the Bolzano bisection lemma; use more metalogic to state it; renamed lemma_Bolzano to Bolzano
20130322, by hoelzl
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
20130322, by hoelzl
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
20130322, by hoelzl
move first_countable_topology to the HOL image
20130322, by hoelzl
move metric_space to its own theory
20130322, by hoelzl
move topological_space to its own theory
20130322, by hoelzl
proper metric for blanks  NB: 70f7483df9cb discontinues coincidence of char_width with space width;
20130321, by wenzelm
eliminated char_width_int to avoid unclear rounding;
20130321, by wenzelm
proofs depend only on constraints, not on def of L WHILE
20130321, by nipkow
less
more

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