Tue, 26 Mar 2013 11:26:13 +0100 wenzelm dockable window for timing information;
Tue, 26 Mar 2013 13:54:24 +0100 kleing no \FIXME macro for ProgProve (moved to book)
Tue, 26 Mar 2013 12:21:01 +0100 hoelzl remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
Tue, 26 Mar 2013 12:21:00 +0100 hoelzl rename eventually_at / _within, to distinguish them from the lemmas in the HOL image
Tue, 26 Mar 2013 12:21:00 +0100 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
Tue, 26 Mar 2013 12:20:59 +0100 hoelzl Series.thy is based on Limits.thy and not Deriv.thy
Tue, 26 Mar 2013 12:20:59 +0100 hoelzl move Ln.thy and Log.thy to Transcendental.thy
Tue, 26 Mar 2013 12:20:58 +0100 hoelzl move SEQ.thy and Lim.thy to Limits.thy
Tue, 26 Mar 2013 12:20:58 +0100 hoelzl HOL-NSA should only import Complex_Main
Tue, 26 Mar 2013 12:20:57 +0100 hoelzl rename RealVector.thy to Real_Vector_Spaces.thy
Tue, 26 Mar 2013 12:20:56 +0100 hoelzl rename RealDef to Real
Tue, 26 Mar 2013 12:20:56 +0100 hoelzl remove Real.thy
Tue, 26 Mar 2013 12:20:55 +0100 hoelzl merge RComplete into RealDef
Tue, 26 Mar 2013 12:20:54 +0100 hoelzl move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings
Tue, 26 Mar 2013 12:20:53 +0100 hoelzl remove posreal_complete
Tue, 26 Mar 2013 12:20:52 +0100 hoelzl separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
Mon, 25 Mar 2013 20:00:27 +0100 ballarin Discontinued theories src/HOL/Algebra/abstract and .../poly.
Mon, 25 Mar 2013 19:53:44 +0100 ballarin Remove obsolete URLs in documentation of HOL-Algebra.
Mon, 25 Mar 2013 19:53:44 +0100 ballarin Fix issue related to mixins in roundup.
Mon, 25 Mar 2013 15:18:44 +0100 kleing simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
Mon, 25 Mar 2013 15:09:41 +0100 nipkow added lemmas
Mon, 25 Mar 2013 14:07:59 +0100 wenzelm merged
Mon, 25 Mar 2013 14:04:01 +0100 wenzelm clarified text_fold vs. fbrk;
Mon, 25 Mar 2013 13:37:44 +0100 wenzelm tuned print_classes: more standard order, markup, formatting;
Mon, 25 Mar 2013 11:05:07 +0100 wenzelm tuned message;
Mon, 25 Mar 2013 10:45:47 +0100 wenzelm actually exit on scalac failure;
Mon, 25 Mar 2013 10:37:38 +0100 wenzelm tuned signature;
Mon, 25 Mar 2013 13:50:50 +0100 kleing removed obsolete uses of ext
Sun, 24 Mar 2013 16:19:54 +0100 wenzelm prefer preset = 3 -- much faster and less memory requirement;
Sun, 24 Mar 2013 16:12:45 +0100 wenzelm basic support for xz files;
Sun, 24 Mar 2013 16:10:19 +0100 wenzelm added component xz-java-1.2;
Sun, 24 Mar 2013 14:26:10 +0100 wenzelm more "quick start" hints;
Sun, 24 Mar 2013 12:07:31 +0100 traytel simple case syntax for stream (stolen from AFP/Coinductive)
Sat, 23 Mar 2013 21:48:03 +0100 wenzelm prefer plain \<^sub> for better rendering (both in Isabelle/jEdit and LaTeX);
Sat, 23 Mar 2013 21:19:10 +0100 wenzelm merged
Sat, 23 Mar 2013 21:13:03 +0100 wenzelm reverted most of 5944b20c41bf -- tends to cause race condition of synchronous vs. asynchronous version;
Sat, 23 Mar 2013 19:54:15 +0100 wenzelm no censorship of "view.fracFontMetrics", although it often degrades rendering quality;
Sat, 23 Mar 2013 19:39:31 +0100 wenzelm retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
Sat, 23 Mar 2013 16:46:09 +0100 wenzelm apply small result immediately, to avoid visible delay of text update after window move;
Sat, 23 Mar 2013 16:10:46 +0100 wenzelm structural equality for Command.Results;
Sat, 23 Mar 2013 13:57:46 +0100 wenzelm allow fractional pretty margin -- avoid premature rounding;
Sat, 23 Mar 2013 13:12:39 +0100 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);
Sat, 23 Mar 2013 13:04:28 +0100 wenzelm tuned;
Sat, 23 Mar 2013 20:57:57 +0100 haftmann spelling
Sat, 23 Mar 2013 20:50:39 +0100 haftmann fundamental revision of big operators on sets
Sat, 23 Mar 2013 17:11:06 +0100 haftmann tuned proof
Sat, 23 Mar 2013 17:11:06 +0100 haftmann locales for abstract orders
Sat, 23 Mar 2013 07:30:53 +0100 krauss merged
Fri, 22 Mar 2013 00:39:16 +0100 krauss added rudimentary induction rule for partial_function (heap)
Fri, 22 Mar 2013 00:39:14 +0100 krauss allow induction predicates with arbitrary arity (not just binary)
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl modernized definition of root: use the_inv, handle positive and negative case uniformly, and 0-th root is constant 0
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl arcsin and arccos are continuous on {0 .. 1} (including the endpoints)
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl move connected to HOL image; used to show intermediate value theorem
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets
Fri, 22 Mar 2013 10:41:43 +0100 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)
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl clean up lemma_nest_unique and renamed to nested_sequence_unique
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl simplify proof of the Bolzano bisection lemma; use more meta-logic to state it; renamed lemma_Bolzano to Bolzano
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip