2014-03-18 wenzelm [Tue, 18 Mar 2014 11:07:47 +0100] rev 56199
tuned signature -- rearranged modules;
src/CCL/CCL.thy src/CCL/Term.thy src/CCL/Type.thy src/Doc/IsarImplementation/ML.thy src/FOLP/IFOLP.thy src/HOL/Bali/AxSem.thy src/HOL/Bali/Eval.thy src/HOL/Bali/Evaln.thy src/HOL/Bali/Example.thy src/HOL/Bali/Term.thy src/HOL/UNITY/Comp/Alloc.thy src/Pure/ML/ml_context.ML src/Pure/ML/ml_thms.ML src/Sequents/Washing.thy

2014-03-18 wenzelm [Tue, 18 Mar 2014 10:00:23 +0100] rev 56198
tuned proofs;
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy

2014-03-17 wenzelm [Mon, 17 Mar 2014 23:16:26 +0100] rev 56197
back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
discontinued obsolete option jedit_completion_dismiss_delay (see 750561986828);
more explicit shutdown;
src/Tools/jEdit/etc/options src/Tools/jEdit/src/completion_popup.scala

2014-03-18 huffman [Tue, 18 Mar 2014 09:39:07 -0700] rev 56196
remove unnecessary finiteness assumptions from lemmas about setsum
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy src/HOL/Multivariate_Analysis/Derivative.thy src/HOL/Multivariate_Analysis/Determinants.thy src/HOL/Multivariate_Analysis/Linear_Algebra.thy

2014-03-18 huffman [Tue, 18 Mar 2014 11:58:30 -0700] rev 56195
adapt to Isabelle/c726ecfb22b6
src/HOL/Decision_Procs/Approximation.thy src/HOL/ex/HarmonicSeries.thy

2014-03-18 hoelzl [Tue, 18 Mar 2014 16:29:32 +0100] rev 56194
fix HOL-NSA; move lemmas
src/HOL/NSA/HSeries.thy src/HOL/NSA/HTranscendental.thy src/HOL/Nat.thy src/HOL/Real_Vector_Spaces.thy src/HOL/Series.thy src/HOL/Set_Interval.thy

2014-03-18 hoelzl [Tue, 18 Mar 2014 15:53:48 +0100] rev 56193
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
src/HOL/MacLaurin.thy src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy src/HOL/Multivariate_Analysis/Derivative.thy src/HOL/Multivariate_Analysis/Integration.thy src/HOL/Probability/Lebesgue_Integration.thy src/HOL/Probability/Lebesgue_Measure.thy src/HOL/Probability/Measure_Space.thy src/HOL/Probability/Projective_Limit.thy src/HOL/Probability/Regularity.thy src/HOL/Series.thy src/HOL/Set_Interval.thy src/HOL/Taylor.thy src/HOL/Transcendental.thy

2014-03-18 traytel [Tue, 18 Mar 2014 14:32:23 +0100] rev 56192
changed policy when to define constants
src/HOL/Tools/BNF/bnf_lfp.ML

2014-03-18 traytel [Tue, 18 Mar 2014 11:47:59 +0100] rev 56191
tuned proofs; removed duplicated facts
src/HOL/BNF_Cardinal_Arithmetic.thy src/HOL/BNF_Cardinal_Order_Relation.thy src/HOL/BNF_Constructions_on_Wellorders.thy src/HOL/Cardinals/Cardinal_Order_Relation.thy

2014-03-18 immler [Tue, 18 Mar 2014 10:12:58 +0100] rev 56190
additional lemmas
src/HOL/Multivariate_Analysis/Integration.thy src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy