2013-03-26 haftmann 2013-03-26 more uniform style for interpretation and sublocale declarations
2013-03-26 wenzelm 2013-03-26 merged
2013-03-26 wenzelm 2013-03-26 tuned session specification;
2013-03-26 wenzelm 2013-03-26 tuned proof;
2013-03-26 wenzelm 2013-03-26 tuned imports;
2013-03-26 wenzelm 2013-03-26 tuned proofs;
2013-03-26 haftmann 2013-03-26 explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
2013-03-26 wenzelm 2013-03-26 merged
2013-03-26 wenzelm 2013-03-26 proper input event handling;
2013-03-26 wenzelm 2013-03-26 more standard imports;
2013-03-26 wenzelm 2013-03-26 more specific Entry painting; ignore theories with all commands below threshold;
2013-03-26 wenzelm 2013-03-26 tuned;
2013-03-26 wenzelm 2013-03-26 mixed theory/command entries; tuned;
2013-03-26 wenzelm 2013-03-26 dockable window for timing information;
2013-03-26 kleing 2013-03-26 no \FIXME macro for ProgProve (moved to book)
2013-03-26 hoelzl 2013-03-26 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
2013-03-26 hoelzl 2013-03-26 rename eventually_at / _within, to distinguish them from the lemmas in the HOL image
2013-03-26 hoelzl 2013-03-26 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 hoelzl 2013-03-26 Series.thy is based on Limits.thy and not Deriv.thy
2013-03-26 hoelzl 2013-03-26 move Ln.thy and Log.thy to Transcendental.thy
2013-03-26 hoelzl 2013-03-26 move SEQ.thy and Lim.thy to Limits.thy
2013-03-26 hoelzl 2013-03-26 HOL-NSA should only import Complex_Main
2013-03-26 hoelzl 2013-03-26 rename RealVector.thy to Real_Vector_Spaces.thy
2013-03-26 hoelzl 2013-03-26 rename RealDef to Real
2013-03-26 hoelzl 2013-03-26 remove Real.thy
2013-03-26 hoelzl 2013-03-26 merge RComplete into RealDef
2013-03-26 hoelzl 2013-03-26 move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings
2013-03-26 hoelzl 2013-03-26 remove posreal_complete
2013-03-26 hoelzl 2013-03-26 separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
2013-03-25 ballarin 2013-03-25 Discontinued theories src/HOL/Algebra/abstract and .../poly.
2013-03-25 ballarin 2013-03-25 Remove obsolete URLs in documentation of HOL-Algebra.
2013-03-25 ballarin 2013-03-25 Fix issue related to mixins in roundup. Previously, mixins were only applied one level down the DFS tree while they should also be applied at the level of declaration. Makes the algorithm consistent with the version presented in the upcoming JAR paper.
2013-03-25 kleing 2013-03-25 simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
2013-03-25 nipkow 2013-03-25 added lemmas
2013-03-25 wenzelm 2013-03-25 merged
2013-03-25 wenzelm 2013-03-25 clarified text_fold vs. fbrk;
2013-03-25 wenzelm 2013-03-25 tuned print_classes: more standard order, markup, formatting; uniform printing of minimal supersort/classrel;
2013-03-25 wenzelm 2013-03-25 tuned message;
2013-03-25 wenzelm 2013-03-25 actually exit on scalac failure;
2013-03-25 wenzelm 2013-03-25 tuned signature;
2013-03-25 kleing 2013-03-25 removed obsolete uses of ext
2013-03-24 wenzelm 2013-03-24 prefer preset = 3 -- much faster and less memory requirement;
2013-03-24 wenzelm 2013-03-24 basic support for xz files;
2013-03-24 wenzelm 2013-03-24 added component xz-java-1.2;
2013-03-24 wenzelm 2013-03-24 more "quick start" hints; more explicit "Testing of changes", instead of convoluted "Building a repository version of Isabelle"; tuned;
2013-03-24 traytel 2013-03-24 simple case syntax for stream (stolen from AFP/Coinductive)
2013-03-23 wenzelm 2013-03-23 prefer plain \<^sub> for better rendering (both in Isabelle/jEdit and LaTeX); tuned proofs;
2013-03-23 wenzelm 2013-03-23 merged
2013-03-23 wenzelm 2013-03-23 reverted most of 5944b20c41bf -- tends to cause race condition of synchronous vs. asynchronous version;
2013-03-23 wenzelm 2013-03-23 no censorship of "view.fracFontMetrics", although it often degrades rendering quality;
2013-03-23 wenzelm 2013-03-23 retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
2013-03-23 wenzelm 2013-03-23 apply small result immediately, to avoid visible delay of text update after window move;
2013-03-23 wenzelm 2013-03-23 structural equality for Command.Results; more general Command.State.eq_content;
2013-03-23 wenzelm 2013-03-23 allow fractional pretty margin -- avoid premature rounding;
2013-03-23 wenzelm 2013-03-23 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); separate JEdit_Lib.pretty_metric, with slightly closer imitation of jEdit;
2013-03-23 wenzelm 2013-03-23 tuned;
2013-03-23 haftmann 2013-03-23 spelling
2013-03-23 haftmann 2013-03-23 fundamental revision of big operators on sets
2013-03-23 haftmann 2013-03-23 tuned proof
2013-03-23 haftmann 2013-03-23 locales for abstract orders