2015-12-01 Andreas Lochbihler [Tue, 01 Dec 2015 12:35:11 +0100] rev 61766
add formalisation of Bourbaki-Witt fixpoint theorem
CONTRIBUTORS NEWS src/HOL/Library/Bourbaki_Witt_Fixpoint.thy src/HOL/Library/Library.thy

2015-12-01 Andreas Lochbihler [Tue, 01 Dec 2015 12:28:02 +0100] rev 61765
add lemmas
src/HOL/Library/Transitive_Closure_Table.thy

2015-12-01 Andreas Lochbihler [Tue, 01 Dec 2015 12:27:16 +0100] rev 61764
strengthen lemma
src/HOL/Library/Transitive_Closure_Table.thy

2015-12-01 paulson <lp15@cam.ac.uk> [Tue, 01 Dec 2015 14:19:25 +0000] rev 61763
Merge

2015-12-01 paulson <lp15@cam.ac.uk> [Tue, 01 Dec 2015 14:09:10 +0000] rev 61762
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
src/HOL/Complex.thy src/HOL/Decision_Procs/MIR.thy src/HOL/Finite_Set.thy src/HOL/Groups.thy src/HOL/Inequalities.thy src/HOL/Library/BigO.thy src/HOL/Library/Float.thy src/HOL/Library/Infinite_Set.thy src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy src/HOL/Multivariate_Analysis/Complex_Transcendental.thy src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy src/HOL/Multivariate_Analysis/Derivative.thy src/HOL/Multivariate_Analysis/Integration.thy src/HOL/Multivariate_Analysis/Path_Connected.thy src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy src/HOL/Multivariate_Analysis/Weierstrass.thy src/HOL/NSA/Examples/NSPrimes.thy src/HOL/Number_Theory/Eratosthenes.thy src/HOL/Number_Theory/Pocklington.thy src/HOL/Number_Theory/Primes.thy src/HOL/Number_Theory/UniqueFactorization.thy src/HOL/Old_Number_Theory/Legacy_GCD.thy src/HOL/Orderings.thy src/HOL/Probability/Lebesgue_Measure.thy src/HOL/Proofs/Extraction/Euclid.thy src/HOL/Real_Vector_Spaces.thy src/HOL/Rings.thy src/HOL/Transcendental.thy src/HOL/ex/Dedekind_Real.thy src/HOL/ex/Sqrt.thy src/HOL/ex/Sqrt_Script.thy

2015-12-01 blanchet [Tue, 01 Dec 2015 13:07:41 +0100] rev 61761
set "transfer_rule" attribute more generously
src/HOL/Tools/Transfer/transfer_bnf.ML

2015-12-01 blanchet [Tue, 01 Dec 2015 13:07:40 +0100] rev 61760
tuned whitespace
src/HOL/Tools/BNF/bnf_comp.ML src/HOL/Tools/BNF/bnf_comp_tactics.ML src/HOL/Tools/BNF/bnf_def.ML src/HOL/Tools/BNF/bnf_def_tactics.ML src/HOL/Tools/BNF/bnf_fp_def_sugar.ML src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML src/HOL/Tools/BNF/bnf_lfp_size.ML src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML

2015-11-30 wenzelm [Mon, 30 Nov 2015 19:12:08 +0100] rev 61759
misc tuning and modernization;
src/HOL/ex/Higher_Order_Logic.thy

2015-11-30 wenzelm [Mon, 30 Nov 2015 15:23:02 +0100] rev 61758
misc tuning and modernization;
src/FOL/ex/First_Order_Logic.thy

2015-11-30 wenzelm [Mon, 30 Nov 2015 14:24:51 +0100] rev 61757
tuned;
src/HOL/ex/ML.thy src/Tools/SML/Examples.thy