| changeset 64113 | 86efd3d4dc98 |
| parent 64097 | 331fbf2a0d2d |
| child 64122 | 74fde524799e |
--- a/NEWS Sat Oct 08 17:30:19 2016 +0200 +++ b/NEWS Sat Oct 08 14:09:53 2016 +0200 @@ -249,6 +249,8 @@ *** HOL *** +* Dedicated syntax LENGTH('a) for length of types. + * New proof method "argo" using the built-in Argo solver based on SMT technology. The method can be used to prove goals of quantifier-free propositional logic, goals based on a combination of quantifier-free