| changeset 7125 | df7cf6e85501 |
| parent 7113 | ab79d9fa8d8e |
| child 7157 | d49318f6c11a |
--- a/NEWS Wed Jul 28 18:55:35 1999 +0200 +++ b/NEWS Wed Jul 28 19:14:33 1999 +0200 @@ -112,6 +112,8 @@ * Many properties of integer multiplication, division and remainder are now available. +* IsaMakefile: the HOL-Real target now builds an actual image; + * New bounded quantifier syntax (input only): ! x < y. P, ! x <= y. P, ? x < y. P, ? x <= y. P