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

NEWS

changeset 8412 | 65f9089f6f71 |

parent 8392 | 5bf82327aa36 |

child 8425 | f03c667cf702 |

--- a/NEWS Fri Mar 10 15:03:05 2000 +0100 +++ b/NEWS Fri Mar 10 17:14:56 2000 +0100 @@ -7,6 +7,8 @@ *** Overview of INCOMPATIBILITIES (see below for more details) *** +* HOL: "case_tac" is now called "cases_tac" (see below) + * HOL: the constant for f``x is now "image" rather than "op ``". @@ -53,6 +55,10 @@ * HOL/ex: new theory Factorization proving the Fundamental Theorem of Arithmetic, by Thomas M Rasmussen; +* There is a new tactic "cases_tac" for case distinctions; it subsumes the +old "case_tac" (no longer available) and "exhaust_tac" (which should no +longer be used). + *** General *** * compression of ML heaps images may now be controlled via -c option