Wed, 27 Mar 2013 16:38:25 +0100 wenzelm more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Wed, 27 Mar 2013 14:50:30 +0100 wenzelm clarified Skip_Proof.cheat_tac: more standard tactic;
Wed, 27 Mar 2013 14:19:18 +0100 wenzelm tuned signature and module arrangement;
Wed, 27 Mar 2013 14:08:03 +0100 wenzelm tuned;
Wed, 27 Mar 2013 11:54:53 +0100 wenzelm tuned GUI;
Wed, 27 Mar 2013 10:55:05 +0100 haftmann centralized various multiset operations in theory multiset;
Tue, 26 Mar 2013 22:09:39 +0100 haftmann avoid odd foundational terms after interpretation;
Tue, 26 Mar 2013 21:53:56 +0100 haftmann more uniform style for interpretation and sublocale declarations
Tue, 26 Mar 2013 20:55:21 +0100 wenzelm merged
Tue, 26 Mar 2013 20:37:32 +0100 wenzelm tuned session specification;
Tue, 26 Mar 2013 20:36:32 +0100 wenzelm tuned proof;
Tue, 26 Mar 2013 20:02:02 +0100 wenzelm tuned imports;
Tue, 26 Mar 2013 19:43:31 +0100 wenzelm tuned proofs;
Tue, 26 Mar 2013 20:49:57 +0100 haftmann explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
Tue, 26 Mar 2013 15:10:28 +0100 wenzelm merged
Tue, 26 Mar 2013 14:38:44 +0100 wenzelm proper input event handling;
Tue, 26 Mar 2013 14:14:39 +0100 wenzelm more standard imports;
Tue, 26 Mar 2013 14:05:08 +0100 wenzelm more specific Entry painting;
Tue, 26 Mar 2013 14:03:31 +0100 wenzelm tuned;
Tue, 26 Mar 2013 12:40:51 +0100 wenzelm mixed theory/command entries;
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;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip