summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

changeset 13824 | e4d8dea6dfc2 |

parent 13815 | 0832792725db |

child 13829 | af0218406395 |

1.1 --- a/NEWS Wed Feb 19 10:53:27 2003 +0100 1.2 +++ b/NEWS Thu Feb 20 11:09:48 2003 +0100 1.3 @@ -401,6 +401,10 @@ 1.4 1.5 * HOL: canonical cases/induct rules for n-tuples (n = 3..7); 1.6 1.7 +* HOL: consolidated and renamed several theories. In particular: 1.8 + Ord.thy has been absorbed into HOL.thy 1.9 + String.thy has been absorbed into List.thy 1.10 + 1.11 * HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A" 1.12 (beware of argument permutation!); 1.13 1.14 @@ -409,7 +413,8 @@ 1.15 * HOL/List: "nodups" renamed to "distinct"; 1.16 1.17 * HOL: added "The" definite description operator; move Hilbert's "Eps" 1.18 -to peripheral theory "Hilbert_Choice"; 1.19 +to peripheral theory "Hilbert_Choice"; some INCOMPATIBILITIES: 1.20 + - Ex_def has changed, now need to use some_eq_ex 1.21 1.22 * HOL: made split_all_tac safe; EXISTING PROOFS MAY FAIL OR LOOP, so 1.23 in this (rare) case use: