equal
deleted
inserted
replaced
1 Isabelle NEWS -- history of user-visible changes |
1 |
2 ================================================ |
2 Isabelle NEWS -- history user-relevant changes |
|
3 ============================================== |
3 |
4 |
4 New in this Isabelle version |
5 New in this Isabelle version |
5 ---------------------------- |
6 ---------------------------- |
6 |
7 |
7 *** Overview of INCOMPATIBILITIES (see below for more details) *** |
8 *** Overview of INCOMPATIBILITIES (see below for more details) *** |
14 called `inj_on'; |
15 called `inj_on'; |
15 |
16 |
16 * HOL: removed duplicate thms in Arith: |
17 * HOL: removed duplicate thms in Arith: |
17 less_imp_add_less should be replaced by trans_less_add1 |
18 less_imp_add_less should be replaced by trans_less_add1 |
18 le_imp_add_le should be replaced by trans_le_add1 |
19 le_imp_add_le should be replaced by trans_le_add1 |
|
20 |
19 |
21 |
20 *** Proof tools *** |
22 *** Proof tools *** |
21 |
23 |
22 * Simplifier: Asm_full_simp_tac is now more aggressive. |
24 * Simplifier: Asm_full_simp_tac is now more aggressive. |
23 1. It will sometimes reorient premises if that increases their power to |
25 1. It will sometimes reorient premises if that increases their power to |
88 * new theory section 'setup' for generic ML setup functions |
90 * new theory section 'setup' for generic ML setup functions |
89 (e.g. package initialization); |
91 (e.g. package initialization); |
90 |
92 |
91 * the distribution now includes Isabelle icons: see |
93 * the distribution now includes Isabelle icons: see |
92 lib/logo/isabelle-{small,tiny}.xpm; |
94 lib/logo/isabelle-{small,tiny}.xpm; |
|
95 |
|
96 * isatool install - install binaries with absolute references to |
|
97 ISABELLE_HOME/bin; |
93 |
98 |
94 |
99 |
95 *** HOL *** |
100 *** HOL *** |
96 |
101 |
97 * HOL/inductive package reorganized and improved: now supports mutual |
102 * HOL/inductive package reorganized and improved: now supports mutual |
223 |
228 |
224 * calling (stac rew i) now fails if "rew" has no effect on the goal |
229 * calling (stac rew i) now fails if "rew" has no effect on the goal |
225 [previously, this check worked only if the rewrite rule was unconditional] |
230 [previously, this check worked only if the rewrite rule was unconditional] |
226 Now rew can involve either definitions or equalities (either == or =). |
231 Now rew can involve either definitions or equalities (either == or =). |
227 |
232 |
|
233 |
228 *** ZF *** |
234 *** ZF *** |
229 |
235 |
230 * theory Main includes everything; INCOMPATIBILITY: theory ZF.thy contains |
236 * theory Main includes everything; INCOMPATIBILITY: theory ZF.thy contains |
231 only the theorems proved on ZF.ML; |
237 only the theorems proved on ZF.ML; |
232 |
238 |