equal
deleted
inserted
replaced
1 Isabelle NEWS -- history user-relevant changes |
1 Isabelle NEWS -- history user-relevant changes |
2 ============================================== |
2 ============================================== |
3 |
3 |
4 New in this Isabelle version |
4 New in this Isabelle version |
5 ---------------------------- |
5 ---------------------------- |
|
6 |
|
7 *** Pure *** |
|
8 |
|
9 * Command "instance" now takes list of definitions in the same |
|
10 manner as the "definition" command. Most notably, object equality is now |
|
11 possible. Type inference is more canonical than it used to be. |
|
12 INCOMPATIBILITY: in some cases explicit type annotations are required. |
|
13 |
6 |
14 |
7 *** HOL *** |
15 *** HOL *** |
8 |
16 |
9 * Constant "card" now with authentic syntax. |
17 * Constant "card" now with authentic syntax. |
10 |
18 |