summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Thu, 04 Dec 1997 12:50:02 +0100 | |

changeset 4361 | c77a484e4f95 |

parent 4360 | 40e5c97e988d |

child 4362 | e10acc395f0d |

pred -> -1

--- a/NEWS Thu Dec 04 12:44:37 1997 +0100 +++ b/NEWS Thu Dec 04 12:50:02 1997 +0100 @@ -155,9 +155,13 @@ it be used with the new `split_asm_tac'. -* HOL/Nat: users are strongly encouraged to write "0 < n" rather than - "n ~= 0". Theorems and proof tools have been modified towards this - `standard'. +* HOL/Arithmetic: + - `pred n' is automatically converted to `n-1'. + Users are strongly encouraged not to use `pred' any longer, + because it will disappear altogether at some point. + - Users are strongly encouraged to write "0 < n" rather than + "n ~= 0". Theorems and proof tools have been modified towards this + `standard'. * HOL/Lists: the function "set_of_list" has been renamed "set" (and its theorems too);