9 months ago immler [Fri, 13 Jul 2018 12:14:26 +0200] rev 68620
relaxed assumptions for dim_image_eq and dim_image_le
src/HOL/Analysis/Euclidean_Space.thy src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy src/HOL/Vector_Spaces.thy

9 months ago paulson [Thu, 12 Jul 2018 17:23:38 +0100] rev 68619
merged

9 months ago paulson <lp15@cam.ac.uk> [Thu, 12 Jul 2018 17:22:39 +0100] rev 68618
de-applying (mostly Set_Interval)
src/HOL/Nat.thy src/HOL/Set_Interval.thy src/HOL/Transitive_Closure.thy

9 months ago nipkow [Thu, 12 Jul 2018 11:23:46 +0200] rev 68617
more economic tagging
src/HOL/Analysis/Brouwer_Fixpoint.thy src/HOL/Analysis/Euclidean_Space.thy src/HOL/Analysis/Inner_Product.thy src/HOL/Analysis/Measure_Space.thy src/HOL/Analysis/Product_Vector.thy src/HOL/Analysis/Topology_Euclidean_Space.thy src/HOL/ROOT

9 months ago paulson <lp15@cam.ac.uk> [Wed, 11 Jul 2018 23:24:25 +0100] rev 68616
de-applying (mostly Quotient)
src/HOL/Analysis/Infinite_Products.thy src/HOL/Quotient.thy

9 months ago paulson <lp15@cam.ac.uk> [Wed, 11 Jul 2018 19:19:00 +0100] rev 68615
de-applying
src/HOL/Limits.thy src/HOL/Quotient.thy src/HOL/Real_Vector_Spaces.thy

9 months ago paulson <lp15@cam.ac.uk> [Wed, 11 Jul 2018 15:36:12 +0100] rev 68614
more de-applying
src/HOL/Limits.thy src/HOL/Nonstandard_Analysis/HSEQ.thy src/HOL/Transcendental.thy

9 months ago paulson <lp15@cam.ac.uk> [Wed, 11 Jul 2018 09:47:09 +0100] rev 68613
patched a continuity proof
src/HOL/Probability/Sinc_Integral.thy

9 months ago paulson [Wed, 11 Jul 2018 09:14:21 +0100] rev 68612
merged

9 months ago paulson <lp15@cam.ac.uk> [Tue, 10 Jul 2018 23:18:08 +0100] rev 68611
de-applying, etc.
src/HOL/Analysis/Inner_Product.thy src/HOL/Analysis/Product_Vector.thy src/HOL/Deriv.thy src/HOL/Limits.thy src/HOL/Nonstandard_Analysis/HLim.thy src/HOL/Nonstandard_Analysis/HTranscendental.thy src/HOL/NthRoot.thy src/HOL/Power.thy src/HOL/Transcendental.thy