equal
deleted
inserted
replaced
|
1 |
1 Isabelle NEWS -- history user-relevant changes |
2 Isabelle NEWS -- history user-relevant changes |
2 ============================================== |
3 ============================================== |
3 |
4 |
4 *** Overview of INCOMPATIBILITIES *** |
5 *** Overview of INCOMPATIBILITIES *** |
5 |
6 |
54 * HOL/Library: a collection of generic theories to be used together |
55 * HOL/Library: a collection of generic theories to be used together |
55 with main HOL; the theory loader path already includes this directory |
56 with main HOL; the theory loader path already includes this directory |
56 by default; the following existing theories have been moved here: |
57 by default; the following existing theories have been moved here: |
57 HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While |
58 HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While |
58 (as While_Combinator), HOL/Lex/Prefix (as List_Prefix); |
59 (as While_Combinator), HOL/Lex/Prefix (as List_Prefix); |
|
60 |
|
61 * added overloaded operations "inverse" and "divide" (infix "/"); |
59 |
62 |
60 * >, >= and \<ge> can now be used for input; they are immediately replaced |
63 * >, >= and \<ge> can now be used for input; they are immediately replaced |
61 by the converse symbol, eg "x > y" by "y < x". |
64 by the converse symbol, eg "x > y" by "y < x". |
62 |
65 |
63 * HOL/typedef: simplified package, provide more useful rules (see also |
66 * HOL/typedef: simplified package, provide more useful rules (see also |