2009-11-19 wenzelm [Thu, 19 Nov 2009 14:46:33 +0100] rev 33766
adapted Local_Theory.define -- eliminated odd thm kind;
src/HOL/Nominal/nominal_primrec.ML src/HOL/Tools/Function/function_core.ML src/HOL/Tools/Function/mutual.ML src/HOL/Tools/Function/size.ML src/HOL/Tools/inductive.ML src/HOL/Tools/inductive_set.ML src/HOL/Tools/primrec.ML src/HOL/Tools/quickcheck_generators.ML src/HOLCF/Tools/fixrec.ML

2009-11-19 wenzelm [Thu, 19 Nov 2009 14:45:56 +0100] rev 33765
Specification.definition: Thm.definitionK marks exactly the high-level end-user result;
src/Pure/Isar/specification.ML

2009-11-19 wenzelm [Thu, 19 Nov 2009 14:44:22 +0100] rev 33764
Local_Theory.define: eliminated slightly odd kind argument -- such low-level definitions should be hardly ever exposed to end-users anyway;
src/Pure/Isar/local_theory.ML src/Pure/Isar/theory_target.ML

2009-11-19 wenzelm [Thu, 19 Nov 2009 13:00:16 +0100] rev 33763
merged

2009-11-19 paulson [Thu, 19 Nov 2009 11:19:25 +0000] rev 33762
merged

2009-11-19 paulson [Thu, 19 Nov 2009 10:58:36 +0000] rev 33761
Minor correction
doc-src/TutorialI/Types/numerics.tex

2009-11-19 wenzelm [Thu, 19 Nov 2009 12:59:32 +0100] rev 33760
some attempts to improve termination of isatest;
Admin/isatest/isatest-makedist

2009-11-19 hoelzl [Thu, 19 Nov 2009 11:57:30 +0100] rev 33759
Added the contributions of Robert Himmelmann to CONTRIBUTIONS and NEWS
CONTRIBUTORS NEWS src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy src/HOL/Multivariate_Analysis/Derivative.thy

2009-11-19 hoelzl [Thu, 19 Nov 2009 11:51:37 +0100] rev 33758
Renamed vector_less_eq_def to the more usual name vector_le_def.
src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy src/HOL/Multivariate_Analysis/Derivative.thy src/HOL/Multivariate_Analysis/Euclidean_Space.thy src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy

2009-11-19 bulwahn [Thu, 19 Nov 2009 10:49:43 +0100] rev 33757
merged