summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

NEWS

changeset 7847 | 5a3fa0c4b215 |

parent 7805 | 0ae9ddc36fe0 |

child 7863 | 8b0aca9bdc26 |

--- a/NEWS Wed Oct 13 15:16:52 1999 +0200 +++ b/NEWS Wed Oct 13 15:18:15 1999 +0200 @@ -17,6 +17,9 @@ * HOL: the predicate "inj" is now defined by translation to "inj_on"; +* HOL/datatype: mutual_induct_tac no longer exists -- + use induct_tac "x_1 ... x_n" instead of mutual_induct_tac ["x_1", ..., "x_n"] + * HOL/typedef: fixed type inference for representing set; type arguments now have to occur explicitly on the rhs as type constraints;