| changeset 6070 | 032babd0120b |
| parent 6069 | a99879bd9f13 |
| child 6131 | 2d9e609abcdb |
--- a/NEWS Thu Jan 07 11:08:29 1999 +0100 +++ b/NEWS Thu Jan 07 18:30:55 1999 +0100 @@ -61,10 +61,10 @@ *** ZF *** * new primrec section allows primitive recursive functions to be given - directly, as in HOL; + directly (as in HOL) over datatypes and the natural numbers; * new tactics induct_tac and exhaust_tac for induction (or case analysis) - on a datatype; + over datatypes and the natural numbers; * the datatype declaration of type T now defines the recursor T_rec;