changeset 67525 | 5d04d7bcd5f6 |
parent 67510 | 9624711ef2de |
child 67591 | 6fd9902057f5 |
--- a/NEWS Mon Jan 29 19:26:14 2018 +0100 +++ b/NEWS Sun Jan 28 16:38:48 2018 +0000 @@ -169,6 +169,13 @@ *** HOL *** +* Clarifed theorem names: + + Min.antimono ~> Min.subset_imp + Max.antimono ~> Max.subset_imp + +Minor INCOMPATIBILITY. + * 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,