changeset 66345 | 882abe912da9 |
parent 66310 | e8d2862ec203 |
child 66424 | 457da4e299de |
--- a/NEWS Sat Aug 05 22:12:41 2017 +0200 +++ b/NEWS Sun Aug 06 15:02:54 2017 +0200 @@ -116,6 +116,11 @@ *** HOL *** +* Command and antiquotation "value" with modified default strategy: +terms without free variables are always evaluated using plain evaluation +only, with no fallback on normalization by evaluation. +Minor INCOMPATIBILITY. + * Notions of squarefreeness, n-th powers, and prime powers in HOL-Computational_Algebra and HOL-Number_Theory.