12 months ago Lars Hupel <lars.hupel@mytum.de> [Fri, 29 Jun 2018 10:24:36 +0200] rev 68530
remove trailing commas
src/Pure/Admin/isabelle_cronjob.scala src/Pure/Tools/server.scala

12 months ago nipkow [Thu, 28 Jun 2018 17:14:52 +0200] rev 68529
added lemmas
src/HOL/Rat.thy src/HOL/Real.thy

12 months ago paulson [Thu, 28 Jun 2018 14:14:05 +0100] rev 68528
merged

12 months ago paulson <lp15@cam.ac.uk> [Thu, 28 Jun 2018 14:13:57 +0100] rev 68527
Generalising and renaming some basic results
src/HOL/Analysis/Arcwise_Connected.thy src/HOL/Analysis/Cauchy_Integral_Theorem.thy src/HOL/Analysis/Complex_Transcendental.thy src/HOL/Analysis/Connected.thy src/HOL/Analysis/Convex_Euclidean_Space.thy src/HOL/Analysis/Derivative.thy src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy src/HOL/Analysis/Great_Picard.thy src/HOL/Analysis/Henstock_Kurzweil_Integration.thy src/HOL/Analysis/Infinite_Products.thy src/HOL/Analysis/Starlike.thy src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy src/HOL/Deriv.thy src/HOL/Fields.thy src/HOL/Library/Extended_Nonnegative_Real.thy src/HOL/List.thy src/HOL/Nonstandard_Analysis/NSA.thy src/HOL/Real.thy src/HOL/Series.thy src/HOL/Transcendental.thy

12 months ago immler [Thu, 28 Jun 2018 13:49:02 +0200] rev 68526
transfer more lemmas
src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy

12 months ago immler [Thu, 28 Jun 2018 13:18:02 +0200] rev 68525
fixed some oversights
src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy

12 months ago immler [Thu, 28 Jun 2018 10:13:54 +0200] rev 68524
avoid duplicate facts, the "trick" was copied without deeper motivation
src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy

12 months ago wenzelm [Wed, 27 Jun 2018 20:31:22 +0200] rev 68523
clarified settings -- avoid hard-wired directories;
tuned documentation;
NEWS etc/settings src/Doc/System/Environment.thy src/Doc/System/Server.thy src/Doc/System/Sessions.thy src/Pure/Thy/sessions.scala

12 months ago immler [Wed, 27 Jun 2018 11:16:43 +0200] rev 68522
example for Types_To_Sets: transfer from type-based linear algebra to subspaces
CONTRIBUTORS NEWS src/HOL/ROOT src/HOL/Types_To_Sets/Examples/Group_On_With.thy src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy

12 months ago immler [Wed, 27 Jun 2018 10:18:03 +0200] rev 68521
added lemmas and transfer rules
src/HOL/Finite_Set.thy src/HOL/Lifting_Set.thy src/HOL/Transfer.thy