equal
deleted
inserted
replaced
1 |
|
2 Isabelle NEWS -- history user-relevant changes |
1 Isabelle NEWS -- history user-relevant changes |
3 ============================================== |
2 ============================================== |
4 |
3 |
5 New in Isabelle2002 (January 2002) |
4 New in Isabelle2002 (January 2002) |
6 ---------------------------------- |
5 ---------------------------------- |
222 * HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A" |
221 * HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A" |
223 (beware of argument permutation!); |
222 (beware of argument permutation!); |
224 |
223 |
225 * HOL: linorder_less_split superseded by linorder_cases; |
224 * HOL: linorder_less_split superseded by linorder_cases; |
226 |
225 |
|
226 * HOL/List: "nodups" renamed to "distinct" |
|
227 |
227 * HOL: added "The" definite description operator; move Hilbert's "Eps" |
228 * HOL: added "The" definite description operator; move Hilbert's "Eps" |
228 to peripheral theory "Hilbert_Choice"; |
229 to peripheral theory "Hilbert_Choice"; |
229 |
230 |
230 * HOL: made split_all_tac safe; EXISTING PROOFS MAY FAIL OR LOOP, so |
231 * HOL: made split_all_tac safe; EXISTING PROOFS MAY FAIL OR LOOP, so |
231 in this (rare) case use: |
232 in this (rare) case use: |