# HG changeset patch
# User wenzelm
# Date 1514639744 -3600
# Node ID a77c0dd8bb7c6fe0b80bb9b651d89829119def6e
# Parent  48ca44fdc038a571f89c0a6756d49a832f0b5e67
tuned whitespace;

diff -r 48ca44fdc038 -r a77c0dd8bb7c NEWS
--- a/NEWS	Fri Dec 29 21:17:43 2017 +0100
+++ b/NEWS	Sat Dec 30 14:15:44 2017 +0100
@@ -120,10 +120,11 @@
 *** HOL ***
 
 * A new command parametric_constant for proving parametricity of
-  non-recursive definitions. For constants that are not fully parametric the
-  command will infer conditions on relations (e.g., bi_unique, bi_total, or
-  type class conditions such as "respects 0") sufficient for parametricity.
-  See ~~/src/HOL/ex/Conditional_Parametricity_Examples for some examples.
+non-recursive definitions. For constants that are not fully parametric
+the command will infer conditions on relations (e.g., bi_unique,
+bi_total, or type class conditions such as "respects 0") sufficient for
+parametricity. See ~~/src/HOL/ex/Conditional_Parametricity_Examples for
+some examples.
 
 * SMT module:
   - The 'smt_oracle' option is now necessary when using the 'smt' method