equal
deleted
inserted
replaced
1 |
1 |
2 Isabelle NEWS -- history user-relevant changes |
2 Isabelle NEWS -- history user-relevant changes |
3 ============================================== |
3 ============================================== |
4 |
4 |
5 *** Overview of INCOMPATIBILITIES *** |
5 *** Overview of INCOMPATIBILITIES *** |
|
6 |
|
7 * HOL: inductive package no longer splits induction rule aggressively, |
|
8 but only as far as specified by the introductions given; the old |
|
9 format may recovered via ML function complete_split_rule or attribute |
|
10 'split_rule (complete)'; |
6 |
11 |
7 * HOL: induct renamed to lfp_induct, lfp_Tarski to lfp_unfold, |
12 * HOL: induct renamed to lfp_induct, lfp_Tarski to lfp_unfold, |
8 gfp_Tarski to gfp_unfold; |
13 gfp_Tarski to gfp_unfold; |
9 |
14 |
10 * HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp; |
15 * HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp; |