author | nipkow |

Thu Dec 04 12:50:02 1997 +0100 (1997-12-04) | |

changeset 4361 | c77a484e4f95 |

parent 4360 | 40e5c97e988d |

child 4362 | e10acc395f0d |

pred -> -1

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