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

author | wenzelm |

Tue, 18 Jul 2000 21:08:20 +0200 | |

changeset 9383 | c21fa1c48de0 |

parent 9382 | 7cea1cb9703e |

child 9384 | 8e8941c491e6 |

* HOL: removed obsolete expand_if = split_if; theorems if_splits =
split_if split_if_asm; datatype package provides theorems foo.splits =
foo.split foo.split_asm for each datatype;

--- a/NEWS Tue Jul 18 14:52:30 2000 +0200 +++ b/NEWS Tue Jul 18 21:08:20 2000 +0200 @@ -33,6 +33,8 @@ * HOL: theory Sexp now in HOL/Induct examples (used to be part of main HOL, but was unused); should better use HOL's datatype package anyway; +* HOL: removed obsolete theorem binding expand_if, use split_if instead; + * HOL/Real: "rabs" replaced by overloaded "abs" function; * HOL/ML: even fewer consts are declared as global (see theories Ord, @@ -140,6 +142,10 @@ * HOL/Calculation: new rules for substitution in inequalities (monotonicity conditions are extracted to be proven terminally); +* HOL: removed obsolete expand_if = split_if; theorems if_splits = +split_if split_if_asm; datatype package provides theorems foo.splits = +foo.split foo.split_asm for each datatype; + * names of theorems etc. may be natural numbers as well; * Provers: intro/elim/dest attributes: changed ! / !! flags to ? / ??;