2015-05-28 paulson <lp15@cam.ac.uk> [Thu, 28 May 2015 14:33:35 +0100] rev 60307
Convex hulls: theorems about interior, etc. And a few simple lemmas.
src/HOL/Complete_Lattices.thy src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy src/HOL/Multivariate_Analysis/Linear_Algebra.thy src/HOL/Real_Vector_Spaces.thy

2015-05-28 blanchet [Thu, 28 May 2015 10:18:46 +0200] rev 60306
made Auto Sledgehammer behave more like the real thing
NEWS src/Doc/Sledgehammer/document/root.tex src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML

2015-05-28 blanchet [Thu, 28 May 2015 09:50:17 +0200] rev 60305
took out Sledgehammer minimizer optimization that breaks things
src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML

2015-05-28 kleing [Thu, 28 May 2015 17:25:57 +1000] rev 60304
modernized (slightly) type compiler in MicroJava
src/HOL/MicroJava/Comp/AuxLemmas.thy src/HOL/MicroJava/Comp/CorrComp.thy src/HOL/MicroJava/Comp/CorrCompTp.thy src/HOL/MicroJava/Comp/Index.thy src/HOL/MicroJava/Comp/LemmasComp.thy src/HOL/MicroJava/Comp/TranslCompTp.thy src/HOL/MicroJava/Comp/TypeInf.thy

2015-05-26 paulson [Tue, 26 May 2015 21:58:04 +0100] rev 60303
New material about paths, and some lemmas
src/HOL/Finite_Set.thy src/HOL/Fun.thy src/HOL/Library/Convex.thy src/HOL/Library/Countable_Set.thy src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy src/HOL/Multivariate_Analysis/Linear_Algebra.thy src/HOL/Multivariate_Analysis/Path_Connected.thy src/HOL/Real_Vector_Spaces.thy

2015-05-25 wenzelm [Mon, 25 May 2015 22:52:17 +0200] rev 60302
removed obsolete RC tags;
.hgtags

2015-05-25 wenzelm [Mon, 25 May 2015 22:11:43 +0200] rev 60301
merged, resolving conflicts in Admin/isatest/settings/afp-poly and src/HOL/Tools/Nitpick/nitpick_model.ML;
Admin/isatest/settings/afp-poly CONTRIBUTORS NEWS src/Doc/Datatypes/Datatypes.thy src/Doc/Isar_Ref/document/root.tex src/Doc/Nitpick/document/root.tex src/Doc/manual.bib src/HOL/Binomial.thy src/HOL/Transcendental.thy

2015-05-25 wenzelm [Mon, 25 May 2015 12:04:43 +0200] rev 60300
Added tag Isabelle2015 for changeset 5ae2a2e74c93
.hgtags

2015-05-23 wenzelm [Sat, 23 May 2015 17:19:37 +0200] rev 60299 Isabelle2015
clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;
NEWS

2015-05-22 wenzelm [Fri, 22 May 2015 18:13:31 +0200] rev 60298
updated Eisbach manual, using version 3149f9146eb5 of its Bitbucket repository;
src/Doc/Eisbach/Manual.thy src/Doc/Eisbach/Preface.thy