# HG changeset patch
# User wenzelm
# Date 1453208447 -3600
# Node ID ca68dc26fbb674015134c80e16a34732ef2725c6
# Parent  7f5579b12b0ab116c7fef1db0321ed5c96adaa9a
tuned;

diff -r 7f5579b12b0a -r ca68dc26fbb6 CONTRIBUTORS
--- a/CONTRIBUTORS	Tue Jan 19 11:46:54 2016 +0100
+++ b/CONTRIBUTORS	Tue Jan 19 14:00:47 2016 +0100
@@ -16,10 +16,10 @@
 
 * Summer 2015 - Winter 2016: Lawrence C Paulson, Cambridge
   General, homology form of Cauchy's integral theorem and supporting material
-  (ported from HOL Light)
+  (ported from HOL Light).
 
 * Winter 2015/16: Gerwin Klein, NICTA
-  print_record command
+  New print_record command.
 
 * Winter 2015: Manuel Eberl, TUM
   The radius of convergence of power series and various summability tests.
diff -r 7f5579b12b0a -r ca68dc26fbb6 NEWS
--- a/NEWS	Tue Jan 19 11:46:54 2016 +0100
+++ b/NEWS	Tue Jan 19 14:00:47 2016 +0100
@@ -194,9 +194,9 @@
 
 *** Isar ***
 
-* Local goals ('have', 'show', 'hence', 'thus') allow structured
-rule statements like fixes/assumes/shows in theorem specifications, but
-the notation is postfix with keywords 'if' (or 'when') and 'for'. For
+* Local goals ('have', 'show', 'hence', 'thus') allow structured rule
+statements like fixes/assumes/shows in theorem specifications, but the
+notation is postfix with keywords 'if' (or 'when') and 'for'. For
 example:
 
   have result: "C x y"
@@ -240,7 +240,8 @@
 
 * The meaning of 'show' with Pure rule statements has changed: premises
 are treated in the sense of 'assume', instead of 'presume'. This means,
-a goal like "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" can be solved completely as follows:
+a goal like "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" can be solved completely as
+follows:
 
   show "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
 
@@ -401,12 +402,12 @@
 * Configuration option rule_insts_schematic has been discontinued
 (intermediate legacy feature in Isabelle2015). INCOMPATIBILITY.
 
-* Abbreviations in type classes now carry proper sort constraint.
-Rare INCOMPATIBILITY in situations where the previous misbehaviour
-has been exploited.
+* Abbreviations in type classes now carry proper sort constraint. Rare
+INCOMPATIBILITY in situations where the previous misbehaviour has been
+exploited.
 
 * Refinement of user-space type system in type classes: pseudo-local
-operations behave more similar to abbreviations.  Potential
+operations behave more similar to abbreviations. Potential
 INCOMPATIBILITY in exotic situations.
 
 
@@ -471,7 +472,8 @@
 
 * Recursive function definitions ('fun', 'function', 'partial_function')
 expose low-level facts of the internal construction only if the option
-"function_internals" is enabled. Rare INCOMPATIBILITY.
+"function_internals" is enabled. Its internal inductive definition is
+also subject to "inductive_internals". Rare INCOMPATIBILITY.
 
 * BNF datatypes ('datatype', 'codatatype', etc.) expose low-level facts
 of the internal construction only if the option "bnf_internals" is
@@ -635,8 +637,8 @@
 
 * Class uniform_space introduces uniform spaces btw topological spaces
 and metric spaces. Minor INCOMPATIBILITY: open_<type>_def needs to be
-introduced in the form of an uniformity. Some constants are more
-general now, it may be necessary to add type class constraints.
+introduced in the form of an uniformity. Some constants are more general
+now, it may be necessary to add type class constraints.
 
   open_real_def \<leadsto> open_dist
   open_complex_def \<leadsto> open_dist
@@ -794,7 +796,7 @@
 performance.
 
 * Property values in etc/symbols may contain spaces, if written with the
-replacement character "␣" (Unicode point 0x2324).  For example:
+replacement character "␣" (Unicode point 0x2324). For example:
 
     \<star>  code: 0x0022c6  group: operator  font: Deja␣Vu␣Sans␣Mono
 
@@ -818,8 +820,8 @@
 is relevant both for Poly/ML and JVM processes.
 
 * Poly/ML default platform architecture may be changed from 32bit to
-64bit via system option ML_system_64. A system restart (and rebuild)
-is required after change.
+64bit via system option ML_system_64. A system restart (and rebuild) is
+required after change.
 
 * Poly/ML 5.6 runs natively on x86-windows and x86_64-windows, which
 both allow larger heap space than former x86-cygwin.