--- 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