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

tuned session specification;
2013-03-26, by wenzelm
tuned proof;
2013-03-26, by wenzelm
tuned imports;
2013-03-26, by wenzelm
tuned proofs;
2013-03-26, by wenzelm
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
2013-03-26, by haftmann
merged
2013-03-26, by wenzelm
proper input event handling;
2013-03-26, by wenzelm
more standard imports;
2013-03-26, by wenzelm
more specific Entry painting;
2013-03-26, by wenzelm
tuned;
2013-03-26, by wenzelm
mixed theory/command entries;
2013-03-26, by wenzelm
dockable window for timing information;
2013-03-26, by wenzelm
no \FIXME macro for ProgProve (moved to book)
2013-03-26, by kleing
remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
2013-03-26, by hoelzl
rename eventually_at / _within, to distinguish them from the lemmas in the HOL image
2013-03-26, by hoelzl
move theorems about compactness of real closed intervals, the intermediate value theorem, and lemmas about continuity of bijective functions from Deriv.thy to Limits.thy
2013-03-26, by hoelzl
Series.thy is based on Limits.thy and not Deriv.thy
2013-03-26, by hoelzl
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

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

isabelle