2011-08-28 huffman [Sun, 28 Aug 2011 09:20:12 -0700] rev 44568
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
NEWS src/HOL/Decision_Procs/Approximation.thy src/HOL/Deriv.thy src/HOL/Library/FrechetDeriv.thy src/HOL/Library/Product_Vector.thy src/HOL/Lim.thy src/HOL/Limits.thy src/HOL/Multivariate_Analysis/Derivative.thy src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy src/HOL/NSA/HSEQ.thy src/HOL/Probability/Caratheodory.thy src/HOL/Probability/Lebesgue_Integration.thy src/HOL/Probability/Radon_Nikodym.thy src/HOL/SEQ.thy src/HOL/Series.thy src/HOL/Transcendental.thy

2011-08-28 haftmann [Sun, 28 Aug 2011 14:16:14 +0200] rev 44567
tuned
src/HOL/Nominal/Nominal.thy

2011-08-28 blanchet [Sun, 28 Aug 2011 13:13:27 +0200] rev 44566
split timeout among ATPs in and add Metis to the mix as backup
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

2011-08-28 wenzelm [Sun, 28 Aug 2011 13:05:34 +0200] rev 44565
more portable cp options, e.g. for non-GNU version on Mac OS X Leopard;
src/Tools/jEdit/lib/Tools/jedit

2011-08-28 wenzelm [Sun, 28 Aug 2011 12:53:31 +0200] rev 44564
tuned positions of ambiguity messages -- less intrusive in IDE view;
src/Pure/Syntax/syntax_phases.ML

2011-08-28 haftmann [Sun, 28 Aug 2011 08:43:25 +0200] rev 44563
tuned
src/HOL/Library/Cset.thy src/HOL/Library/Dlist_Cset.thy

2011-08-28 haftmann [Sun, 28 Aug 2011 08:13:58 +0200] rev 44562
merged

2011-08-28 haftmann [Sun, 28 Aug 2011 08:13:30 +0200] rev 44561
avoid loading List_Cset and Dlist_Cet at the same time
src/HOL/Library/Library.thy src/HOL/Library/ROOT.ML

2011-08-28 haftmann [Sun, 28 Aug 2011 08:12:54 +0200] rev 44560
corrected slip
src/HOL/Library/List_Cset.thy

2011-08-27 haftmann [Sat, 27 Aug 2011 19:52:58 +0200] rev 44559
Cset, Dlist_Cset, List_Cset: restructured