| changeset 12889 | 1de4f0b824a8 |
| parent 12877 | b9635eb8a448 |
| child 12899 | 7d5b690253ee |
--- a/NEWS Thu Feb 14 12:06:07 2002 +0100 +++ b/NEWS Thu Feb 14 12:24:02 2002 +0100 @@ -1,4 +1,3 @@ - Isabelle NEWS -- history user-relevant changes ============================================== @@ -224,6 +223,8 @@ * HOL: linorder_less_split superseded by linorder_cases; +* HOL/List: "nodups" renamed to "distinct" + * HOL: added "The" definite description operator; move Hilbert's "Eps" to peripheral theory "Hilbert_Choice";