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 * Provers/trancl.ML: new transitivity reasoner for transitive and |
|
10 reflexive-transitive closure of relations. |
8 |
11 |
9 * Pure: considerably improved version of 'constdefs' command. Now |
12 * Pure: considerably improved version of 'constdefs' command. Now |
10 performs automatic type-inference of declared constants; additional |
13 performs automatic type-inference of declared constants; additional |
11 support for local structure declarations (cf. locales and HOL |
14 support for local structure declarations (cf. locales and HOL |
12 records), see also isar-ref manual. Potential INCOMPATIBILITY: need |
15 records), see also isar-ref manual. Potential INCOMPATIBILITY: need |
182 '\<Sum>x<k. e' is the same as 'setsum (%x. e) {..<k}' |
185 '\<Sum>x<k. e' is the same as 'setsum (%x. e) {..<k}' |
183 |
186 |
184 Function 'Summation' over nat is gone, its syntax '\<Sum>i<k. e' |
187 Function 'Summation' over nat is gone, its syntax '\<Sum>i<k. e' |
185 now translates into 'setsum' as above. |
188 now translates into 'setsum' as above. |
186 |
189 |
|
190 * Simplifier: |
|
191 - Is now set up to reason about transitivity chains involving "trancl" (r^+) |
|
192 and "rtrancl" (r^*) by setting up tactics provided by Provers/trancl.ML |
|
193 as additional solvers. |
|
194 - INCOMPATIBILITY: old proofs break occasionally. Typically, this is |
|
195 because simplification now solves more goals than previously. |
187 |
196 |
188 *** HOLCF *** |
197 *** HOLCF *** |
189 |
198 |
190 * HOLCF: discontinued special version of 'constdefs' (which used to |
199 * HOLCF: discontinued special version of 'constdefs' (which used to |
191 support continuous functions) in favor of the general Pure one with |
200 support continuous functions) in favor of the general Pure one with |