tuned whitespace;
authorwenzelm
Sat Dec 30 14:15:44 2017 +0100 (17 months ago)
changeset 67303a77c0dd8bb7c
parent 67302 48ca44fdc038
child 67304 3cf05d7cf174
tuned whitespace;
NEWS
     1.1 --- a/NEWS	Fri Dec 29 21:17:43 2017 +0100
     1.2 +++ b/NEWS	Sat Dec 30 14:15:44 2017 +0100
     1.3 @@ -120,10 +120,11 @@
     1.4  *** HOL ***
     1.5  
     1.6  * A new command parametric_constant for proving parametricity of
     1.7 -  non-recursive definitions. For constants that are not fully parametric the
     1.8 -  command will infer conditions on relations (e.g., bi_unique, bi_total, or
     1.9 -  type class conditions such as "respects 0") sufficient for parametricity.
    1.10 -  See ~~/src/HOL/ex/Conditional_Parametricity_Examples for some examples.
    1.11 +non-recursive definitions. For constants that are not fully parametric
    1.12 +the command will infer conditions on relations (e.g., bi_unique,
    1.13 +bi_total, or type class conditions such as "respects 0") sufficient for
    1.14 +parametricity. See ~~/src/HOL/ex/Conditional_Parametricity_Examples for
    1.15 +some examples.
    1.16  
    1.17  * SMT module:
    1.18    - The 'smt_oracle' option is now necessary when using the 'smt' method