hoelzl [Tue, 26 Mar 2013 12:20:53 +0100] rev 51519
remove posreal_complete
hoelzl [Tue, 26 Mar 2013 12:20:52 +0100] rev 51518
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
ballarin [Mon, 25 Mar 2013 20:00:27 +0100] rev 51517
Discontinued theories src/HOL/Algebra/abstract and .../poly.
ballarin [Mon, 25 Mar 2013 19:53:44 +0100] rev 51516
Remove obsolete URLs in documentation of HOL-Algebra.
ballarin [Mon, 25 Mar 2013 19:53:44 +0100] rev 51515
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.
kleing [Mon, 25 Mar 2013 15:18:44 +0100] rev 51514
simp_const -> afold; bfold -> fold'; bsimp_const -> bfold
nipkow [Mon, 25 Mar 2013 15:09:41 +0100] rev 51513
added lemmas
wenzelm [Mon, 25 Mar 2013 14:07:59 +0100] rev 51512
merged
wenzelm [Mon, 25 Mar 2013 14:04:01 +0100] rev 51511
clarified text_fold vs. fbrk;
wenzelm [Mon, 25 Mar 2013 13:37:44 +0100] rev 51510
tuned print_classes: more standard order, markup, formatting;
uniform printing of minimal supersort/classrel;
wenzelm [Mon, 25 Mar 2013 11:05:07 +0100] rev 51509
tuned message;
wenzelm [Mon, 25 Mar 2013 10:45:47 +0100] rev 51508
actually exit on scalac failure;
wenzelm [Mon, 25 Mar 2013 10:37:38 +0100] rev 51507
tuned signature;
kleing [Mon, 25 Mar 2013 13:50:50 +0100] rev 51506
removed obsolete uses of ext
wenzelm [Sun, 24 Mar 2013 16:19:54 +0100] rev 51505
prefer preset = 3 -- much faster and less memory requirement;
wenzelm [Sun, 24 Mar 2013 16:12:45 +0100] rev 51504
basic support for xz files;
wenzelm [Sun, 24 Mar 2013 16:10:19 +0100] rev 51503
added component xz-java-1.2;
wenzelm [Sun, 24 Mar 2013 14:26:10 +0100] rev 51502
more "quick start" hints;
more explicit "Testing of changes", instead of convoluted "Building a repository version of Isabelle";
tuned;
traytel [Sun, 24 Mar 2013 12:07:31 +0100] rev 51501
simple case syntax for stream (stolen from AFP/Coinductive)
wenzelm [Sat, 23 Mar 2013 21:48:03 +0100] rev 51500
prefer plain \<^sub> for better rendering (both in Isabelle/jEdit and LaTeX);
tuned proofs;
wenzelm [Sat, 23 Mar 2013 21:19:10 +0100] rev 51499
merged
wenzelm [Sat, 23 Mar 2013 21:13:03 +0100] rev 51498
reverted most of 5944b20c41bf -- tends to cause race condition of synchronous vs. asynchronous version;
wenzelm [Sat, 23 Mar 2013 19:54:15 +0100] rev 51497
no censorship of "view.fracFontMetrics", although it often degrades rendering quality;
wenzelm [Sat, 23 Mar 2013 19:39:31 +0100] rev 51496
retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
wenzelm [Sat, 23 Mar 2013 16:46:09 +0100] rev 51495
apply small result immediately, to avoid visible delay of text update after window move;
wenzelm [Sat, 23 Mar 2013 16:10:46 +0100] rev 51494
structural equality for Command.Results;
more general Command.State.eq_content;
wenzelm [Sat, 23 Mar 2013 13:57:46 +0100] rev 51493
allow fractional pretty margin -- avoid premature rounding;
wenzelm [Sat, 23 Mar 2013 13:12:39 +0100] rev 51492
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;
wenzelm [Sat, 23 Mar 2013 13:04:28 +0100] rev 51491
tuned;
haftmann [Sat, 23 Mar 2013 20:57:57 +0100] rev 51490
spelling