2016-10-01 wenzelm [Sat, 01 Oct 2016 17:38:14 +0200] rev 63980
Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);
src/HOL/BNF_Cardinal_Order_Relation.thy src/HOL/Hilbert_Choice.thy src/HOL/Inductive.thy src/HOL/Isar_Examples/Schroeder_Bernstein.thy src/HOL/ROOT

2016-10-01 wenzelm [Sat, 01 Oct 2016 17:16:35 +0200] rev 63979
clarified lfp/gfp statements and proofs;
NEWS src/HOL/Complete_Partial_Order.thy src/HOL/Inductive.thy src/HOL/Library/Extended_Nonnegative_Real.thy src/HOL/Library/Order_Continuity.thy src/HOL/Nat.thy

2016-10-01 Lars Hupel <lars.hupel@mytum.de> [Sat, 01 Oct 2016 15:21:43 +0200] rev 63978
repair LaTeX
src/HOL/Analysis/Path_Connected.thy

2016-10-01 wenzelm [Sat, 01 Oct 2016 12:03:27 +0200] rev 63977
misc tuning for release;
NEWS

2016-10-01 wenzelm [Sat, 01 Oct 2016 11:14:00 +0200] rev 63976
added lemma;
src/HOL/Inductive.thy

2016-09-30 paulson <lp15@cam.ac.uk> [Fri, 30 Sep 2016 17:12:50 +0100] rev 63975
Trying out "subgoal", and no more [| |]
src/HOL/Auth/OtwayRees.thy

2016-09-30 hoelzl [Fri, 30 Sep 2016 15:51:43 +0200] rev 63974
HOL-Analysis: fix latex generation
src/HOL/Analysis/Path_Connected.thy

2016-09-30 hoelzl [Fri, 30 Sep 2016 15:35:46 +0200] rev 63973
Probability: fix proof
src/HOL/Probability/Probability_Mass_Function.thy

2016-09-30 hoelzl [Fri, 30 Sep 2016 15:35:43 +0200] rev 63972
Library: fix name Product_plus to Product_Plus
src/HOL/Analysis/Product_Vector.thy src/HOL/Library/Library.thy src/HOL/Library/Product_Order.thy src/HOL/Library/Product_Plus.thy src/HOL/Library/Product_plus.thy

2016-09-30 hoelzl [Fri, 30 Sep 2016 15:35:37 +0200] rev 63971
HOL-Analysis: move Product_Vector and Inner_Product from Library
src/HOL/Analysis/Convex_Euclidean_Space.thy src/HOL/Analysis/Euclidean_Space.thy src/HOL/Analysis/Inner_Product.thy src/HOL/Analysis/Product_Vector.thy src/HOL/Library/Inner_Product.thy src/HOL/Library/Library.thy src/HOL/Library/Product_Vector.thy src/HOL/Mirabelle/ex/Ex.thy