6 ---------------------------- |
6 ---------------------------- |
7 |
7 |
8 *** Overview of INCOMPATIBILITIES (see below for more details) *** |
8 *** Overview of INCOMPATIBILITIES (see below for more details) *** |
9 |
9 |
10 * several changes of proof tools; |
10 * several changes of proof tools; |
|
11 |
|
12 * HOL: new version of inductive and datatype; |
11 |
13 |
12 * HOL: major changes to the inductive and datatype packages; |
14 * HOL: major changes to the inductive and datatype packages; |
13 |
15 |
14 * HOL: renamed r^-1 to 'converse' from 'inverse'; `inj_onto' is now |
16 * HOL: renamed r^-1 to 'converse' from 'inverse'; `inj_onto' is now |
15 called `inj_on'; |
17 called `inj_on'; |
260 * Pure: several new basic modules made available for general use, see |
262 * Pure: several new basic modules made available for general use, see |
261 also src/Pure/README; |
263 also src/Pure/README; |
262 |
264 |
263 * improved the theory data mechanism to support encapsulation (data |
265 * improved the theory data mechanism to support encapsulation (data |
264 kind name replaced by private Object.kind, acting as authorization |
266 kind name replaced by private Object.kind, acting as authorization |
265 key); new type-safe user interface via functor TheoryDataFun; |
267 key); new type-safe user interface via functor TheoryDataFun; generic |
|
268 print_data function becomes basically useless; |
266 |
269 |
267 * removed global_names compatibility flag -- all theory declarations |
270 * removed global_names compatibility flag -- all theory declarations |
268 are qualified by default; |
271 are qualified by default; |
269 |
272 |
270 * module Pure/Syntax now offers quote / antiquote translation |
273 * module Pure/Syntax now offers quote / antiquote translation |
271 functions (useful for Hoare logic etc. with implicit dependencies); |
274 functions (useful for Hoare logic etc. with implicit dependencies); |
|
275 see HOL/ex/Antiquote for an example use; |
272 |
276 |
273 * Simplifier now offers conversions (asm_)(full_)rewrite: simpset -> |
277 * Simplifier now offers conversions (asm_)(full_)rewrite: simpset -> |
274 cterm -> thm; |
278 cterm -> thm; |
275 |
279 |
276 * new tactical CHANGED_GOAL for checking that a tactic modifies a |
280 * new tactical CHANGED_GOAL for checking that a tactic modifies a |