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 Isabelle2001 (December 2001) |
4 New in Isabelle2001 (December 2001) |
6 ----------------------------------- |
5 ----------------------------------- |
222 * HOL: introduced f^n = f o ... o f; warning: due to the limits of |
221 * HOL: introduced f^n = f o ... o f; warning: due to the limits of |
223 Isabelle's type classes, ^ on functions and relations has too general |
222 Isabelle's type classes, ^ on functions and relations has too general |
224 a domain, namely ('a * 'b) set and 'a => 'b; this means that it may be |
223 a domain, namely ('a * 'b) set and 'a => 'b; this means that it may be |
225 necessary to attach explicit type constraints; |
224 necessary to attach explicit type constraints; |
226 |
225 |
|
226 * HOL/Relation: the prefix name of the infix "O" has been changed from "comp" |
|
227 to "rel_comp"; INCOMPATIBILITY: a few theorems have been renamed accordingly |
|
228 (eg "compI" -> "rel_compI"). |
|
229 |
227 * HOL: syntax translations now work properly with numerals and records |
230 * HOL: syntax translations now work properly with numerals and records |
228 expressions; |
231 expressions; |
229 |
232 |
230 * HOL: bounded abstraction now uses syntax "%" / "\<lambda>" instead |
233 * HOL: bounded abstraction now uses syntax "%" / "\<lambda>" instead |
231 of "lam" -- INCOMPATIBILITY; |
234 of "lam" -- INCOMPATIBILITY; |