equal
deleted
inserted
replaced
3 |
3 |
4 New in this Isabelle release |
4 New in this Isabelle release |
5 ---------------------------- |
5 ---------------------------- |
6 |
6 |
7 *** General *** |
7 *** General *** |
|
8 |
|
9 * Pure: Simplification procedures can now take the current simpset as |
|
10 an additional argument; This is useful for calling the simplifier |
|
11 recursively. See the functions MetaSimplifier.full_{mk_simproc, |
|
12 simproc,simproc_i}. |
8 |
13 |
9 * Pure: considerably improved version of 'constdefs' command. Now |
14 * Pure: considerably improved version of 'constdefs' command. Now |
10 performs automatic type-inference of declared constants; additional |
15 performs automatic type-inference of declared constants; additional |
11 support for local structure declarations (cf. locales and HOL |
16 support for local structure declarations (cf. locales and HOL |
12 records), see also isar-ref manual. Potential INCOMPATIBILITY: need |
17 records), see also isar-ref manual. Potential INCOMPATIBILITY: need |