12 hours ago nipkow [Mon, 24 Sep 2018 23:49:43 +0200] rev 69067 default tip
merged

12 hours ago nipkow [Mon, 24 Sep 2018 23:27:01 +0200] rev 69066
NEWS
NEWS

19 hours ago nipkow [Mon, 24 Sep 2018 16:09:27 +0200] rev 69065
more conversion from ( * ) to (*)
src/Doc/Isar_Ref/Inner_Syntax.thy src/Doc/Locales/Examples3.thy src/Doc/Main/Main_Doc.thy src/HOL/SMT_Examples/boogie.ML

21 hours ago nipkow [Mon, 24 Sep 2018 14:30:09 +0200] rev 69064
Prefix form of infix with * on either side no longer needs special treatment
because (* and *) are no longer comment brackets in terms.
src/HOL/Algebra/IntRing.thy src/HOL/Algebra/Sym_Groups.thy src/HOL/Algebra/UnivPoly.thy src/HOL/Analysis/Ball_Volume.thy src/HOL/Analysis/Bochner_Integration.thy src/HOL/Analysis/Bounded_Linear_Function.thy src/HOL/Analysis/Cartesian_Euclidean_Space.thy src/HOL/Analysis/Cartesian_Space.thy src/HOL/Analysis/Cauchy_Integral_Theorem.thy src/HOL/Analysis/Change_Of_Vars.thy src/HOL/Analysis/Complex_Analysis_Basics.thy src/HOL/Analysis/Conformal_Mappings.thy src/HOL/Analysis/Connected.thy src/HOL/Analysis/Convex_Euclidean_Space.thy src/HOL/Analysis/Derivative.thy src/HOL/Analysis/Determinants.thy src/HOL/Analysis/Euclidean_Space.thy src/HOL/Analysis/Finite_Cartesian_Product.thy src/HOL/Analysis/Finite_Product_Measure.thy src/HOL/Analysis/Further_Topology.thy src/HOL/Analysis/Gamma_Function.thy src/HOL/Analysis/Harmonic_Numbers.thy src/HOL/Analysis/Henstock_Kurzweil_Integration.thy src/HOL/Analysis/Homeomorphism.thy src/HOL/Analysis/Inner_Product.thy src/HOL/Analysis/Lebesgue_Measure.thy src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy src/HOL/Analysis/Path_Connected.thy src/HOL/Analysis/Product_Vector.thy src/HOL/Analysis/Riemann_Mapping.thy src/HOL/Analysis/Starlike.thy src/HOL/Analysis/normarith.ML src/HOL/Binomial.thy src/HOL/Computational_Algebra/Euclidean_Algorithm.thy src/HOL/Computational_Algebra/Formal_Power_Series.thy src/HOL/Computational_Algebra/Polynomial.thy src/HOL/Decision_Procs/Algebra_Aux.thy src/HOL/Decision_Procs/Cooper.thy src/HOL/Decision_Procs/Ferrack.thy src/HOL/Decision_Procs/MIR.thy src/HOL/Decision_Procs/Polynomial_List.thy src/HOL/Deriv.thy src/HOL/Enum.thy src/HOL/Factorial.thy src/HOL/GCD.thy src/HOL/Groups_List.thy src/HOL/Library/Code_Real_Approx_By_Float.thy src/HOL/Library/DAList_Multiset.thy src/HOL/Library/Discrete.thy src/HOL/Library/Extended_Nonnegative_Real.thy ...

13 hours ago wenzelm [Mon, 24 Sep 2018 22:10:24 +0200] rev 69063
expose locale_dependency information;
src/Pure/Isar/locale.ML

13 hours ago wenzelm [Mon, 24 Sep 2018 22:05:25 +0200] rev 69062
tuned signature;
src/Pure/Isar/locale.ML src/Pure/morphism.ML

15 hours ago wenzelm [Mon, 24 Sep 2018 20:24:03 +0200] rev 69061
tuned signature: more explicit types;
src/Pure/Isar/locale.ML

15 hours ago wenzelm [Mon, 24 Sep 2018 20:05:41 +0200] rev 69060
tuned;
src/Pure/Isar/locale.ML

16 hours ago wenzelm [Mon, 24 Sep 2018 19:53:45 +0200] rev 69059
tuned signature: prefer value-oriented pretty-printing;
src/Pure/Isar/locale.ML src/Pure/Pure.thy

16 hours ago wenzelm [Mon, 24 Sep 2018 19:43:20 +0200] rev 69058
tuned signature;
src/Pure/Isar/class.ML src/Pure/Isar/class_declaration.ML src/Pure/Isar/interpretation.ML src/Pure/Isar/local_theory.ML src/Pure/Isar/locale.ML