2015-04-01 paulson <lp15@cam.ac.uk> [Wed, 01 Apr 2015 14:48:38 +0100] rev 59870
HOL Light Libraries for complex Arctan, Arcsin, Arccos
NEWS src/HOL/Multivariate_Analysis/Complex_Transcendental.thy

2015-04-01 paulson <lp15@cam.ac.uk> [Wed, 01 Apr 2015 14:08:17 +0100] rev 59869
arcsin and arccos lemmas
src/HOL/Transcendental.thy

2015-03-31 haftmann [Tue, 31 Mar 2015 21:54:32 +0200] rev 59868
NEWS
NEWS

2015-03-31 haftmann [Tue, 31 Mar 2015 21:54:32 +0200] rev 59867
given up separate type classes demanding `inverse 0 = 0`
src/HOL/Binomial.thy src/HOL/Complex.thy src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy src/HOL/Decision_Procs/Rat_Pair.thy src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy src/HOL/Deriv.thy src/HOL/Enum.thy src/HOL/Fields.thy src/HOL/Groups_Big.thy src/HOL/Library/BigO.thy src/HOL/Library/Bit.thy src/HOL/Library/Formal_Power_Series.thy src/HOL/Library/Fraction_Field.thy src/HOL/Limits.thy src/HOL/Metis_Examples/Big_O.thy src/HOL/Multivariate_Analysis/Determinants.thy src/HOL/Multivariate_Analysis/PolyRoots.thy src/HOL/NSA/HDeriv.thy src/HOL/NSA/HyperDef.thy src/HOL/NSA/NSA.thy src/HOL/NSA/StarDef.thy src/HOL/Num.thy src/HOL/Numeral_Simprocs.thy src/HOL/Power.thy src/HOL/Probability/Bochner_Integration.thy src/HOL/Probability/Interval_Integral.thy src/HOL/Probability/Set_Integral.thy src/HOL/Quotient_Examples/Quotient_Rat.thy src/HOL/Rat.thy src/HOL/Real.thy src/HOL/Real_Vector_Spaces.thy src/HOL/Tools/numeral_simprocs.ML src/HOL/Transcendental.thy src/HOL/ex/Dedekind_Real.thy src/HOL/ex/Simproc_Tests.thy

2015-03-31 paulson <lp15@cam.ac.uk> [Tue, 31 Mar 2015 16:49:41 +0100] rev 59866
Merge

2015-03-31 paulson <lp15@cam.ac.uk> [Tue, 31 Mar 2015 16:48:48 +0100] rev 59865
rationalised and generalised some theorems concerning abs and x^2.
src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy src/HOL/Multivariate_Analysis/Linear_Algebra.thy src/HOL/Power.thy src/HOL/Rings.thy src/HOL/Transcendental.thy

2015-03-31 nipkow [Tue, 31 Mar 2015 17:29:44 +0200] rev 59864
added lemmas
src/HOL/HOL.thy

2015-03-31 paulson <lp15@cam.ac.uk> [Tue, 31 Mar 2015 15:01:06 +0100] rev 59863
Merge

2015-03-31 paulson <lp15@cam.ac.uk> [Tue, 31 Mar 2015 15:00:03 +0100] rev 59862
New material and binomial fix
src/HOL/Binomial.thy src/HOL/Complex.thy src/HOL/Deriv.thy src/HOL/Library/Convex.thy src/HOL/Library/Formal_Power_Series.thy src/HOL/Multivariate_Analysis/Complex_Transcendental.thy src/HOL/Transcendental.thy

2015-03-31 blanchet [Tue, 31 Mar 2015 14:42:06 +0200] rev 59861
tuned doc
src/Doc/Datatypes/Datatypes.thy