isabelle: Graph

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

move Ln.thy and Log.thy to Transcendental.thy
2013-03-26, by hoelzl
move SEQ.thy and Lim.thy to Limits.thy
2013-03-26, by hoelzl
HOL-NSA should only import Complex_Main
2013-03-26, by hoelzl
rename RealVector.thy to Real_Vector_Spaces.thy
2013-03-26, by hoelzl
rename RealDef to Real
2013-03-26, by hoelzl
remove Real.thy
2013-03-26, by hoelzl
merge RComplete into RealDef
2013-03-26, by hoelzl
move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings
2013-03-26, by hoelzl
remove posreal_complete
2013-03-26, by hoelzl
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
2013-03-26, by hoelzl
Discontinued theories src/HOL/Algebra/abstract and .../poly.
2013-03-25, by ballarin
Remove obsolete URLs in documentation of HOL-Algebra.
2013-03-25, by ballarin
Fix issue related to mixins in roundup.
2013-03-25, by ballarin
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
2013-03-25, by kleing
added lemmas
2013-03-25, by nipkow
merged
2013-03-25, by wenzelm
clarified text_fold vs. fbrk;
2013-03-25, by wenzelm
tuned print_classes: more standard order, markup, formatting;
2013-03-25, by wenzelm
tuned message;
2013-03-25, by wenzelm
actually exit on scalac failure;
2013-03-25, by wenzelm
tuned signature;
2013-03-25, by wenzelm
removed obsolete uses of ext
2013-03-25, by kleing
prefer preset = 3 -- much faster and less memory requirement;
2013-03-24, by wenzelm
basic support for xz files;
2013-03-24, by wenzelm
added component xz-java-1.2;
2013-03-24, by wenzelm
more "quick start" hints;
2013-03-24, by wenzelm
simple case syntax for stream (stolen from AFP/Coinductive)
2013-03-24, by traytel
prefer plain \<^sub> for better rendering (both in Isabelle/jEdit and LaTeX);
2013-03-23, by wenzelm
merged
2013-03-23, by wenzelm
reverted most of 5944b20c41bf -- tends to cause race condition of synchronous vs. asynchronous version;
2013-03-23, by wenzelm
no censorship of "view.fracFontMetrics", although it often degrades rendering quality;
2013-03-23, by wenzelm
retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
2013-03-23, by wenzelm
apply small result immediately, to avoid visible delay of text update after window move;
2013-03-23, by wenzelm
structural equality for Command.Results;
2013-03-23, by wenzelm
allow fractional pretty margin -- avoid premature rounding;
2013-03-23, 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);
2013-03-23, by wenzelm
tuned;
2013-03-23, by wenzelm
spelling
2013-03-23, by haftmann
fundamental revision of big operators on sets
2013-03-23, by haftmann
tuned proof
2013-03-23, by haftmann
locales for abstract orders
2013-03-23, by haftmann
merged
2013-03-23, by krauss
added rudimentary induction rule for partial_function (heap)
2013-03-22, by krauss
allow induction predicates with arbitrary arity (not just binary)
2013-03-22, by krauss
modernized definition of root: use the_inv, handle positive and negative case uniformly, and 0-th root is constant 0
2013-03-22, by hoelzl
arcsin and arccos are continuous on {0 .. 1} (including the endpoints)
2013-03-22, by hoelzl
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
2013-03-22, by hoelzl
move connected to HOL image; used to show intermediate value theorem
2013-03-22, 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
2013-03-22, 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)
2013-03-22, by hoelzl
clean up lemma_nest_unique and renamed to nested_sequence_unique
2013-03-22, by hoelzl
simplify proof of the Bolzano bisection lemma; use more meta-logic to state it; renamed lemma_Bolzano to Bolzano
2013-03-22, by hoelzl
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
2013-03-22, by hoelzl
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
2013-03-22, by hoelzl
move first_countable_topology to the HOL image
2013-03-22, by hoelzl
move metric_space to its own theory
2013-03-22, by hoelzl
move topological_space to its own theory
2013-03-22, by hoelzl
proper metric for blanks -- NB: 70f7483df9cb discontinues coincidence of char_width with space width;
2013-03-21, by wenzelm
eliminated char_width_int to avoid unclear rounding;
2013-03-21, by wenzelm
proofs depend only on constraints, not on def of L WHILE
2013-03-21, by nipkow

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle