equal
deleted
inserted
replaced
5 New in Isabelle99-2 (February 2001) |
5 New in Isabelle99-2 (February 2001) |
6 ----------------------------------- |
6 ----------------------------------- |
7 |
7 |
8 *** Overview of INCOMPATIBILITIES *** |
8 *** Overview of INCOMPATIBILITIES *** |
9 |
9 |
|
10 * HOL/Algebra: special summation operator SUM no longer exists, it has |
|
11 been replaced by setsum; infix 'assoc' now has priority 50 (like 'dvd'); |
|
12 |
|
13 * HOL/Algebra: axiom 'one_not_zero' has been moved from axclass 'ring' |
|
14 to 'domain', this makes the theory consistent with mathematical literature; |
|
15 |
10 * HOL: inductive package no longer splits induction rule aggressively, |
16 * HOL: inductive package no longer splits induction rule aggressively, |
11 but only as far as specified by the introductions given; the old |
17 but only as far as specified by the introductions given; the old |
12 format may recovered via ML function complete_split_rule or attribute |
18 format may recovered via ML function complete_split_rule or attribute |
13 'split_rule (complete)'; |
19 'split_rule (complete)'; |
14 |
20 |