equal
deleted
inserted
replaced
|
1 |
1 Isabelle NEWS -- history user-relevant changes |
2 Isabelle NEWS -- history user-relevant changes |
2 ============================================== |
3 ============================================== |
3 |
4 |
4 New in this Isabelle release |
5 New in this Isabelle release |
5 ---------------------------- |
6 ---------------------------- |
26 |
27 |
27 * Provers: improved induct method: assumptions introduced by case |
28 * Provers: improved induct method: assumptions introduced by case |
28 "foo" are split into "foo.hyps" (from the rule) and "foo.prems" (from |
29 "foo" are split into "foo.hyps" (from the rule) and "foo.prems" (from |
29 the goal statement); "foo" still refers to all facts collectively; |
30 the goal statement); "foo" still refers to all facts collectively; |
30 |
31 |
|
32 * Isar: preview of problems to finish 'show' now produce an error |
|
33 rather than just a warning (in interactive mode); |
|
34 |
31 |
35 |
32 *** HOL *** |
36 *** HOL *** |
33 |
37 |
34 * 'typedef' command has new option "open" to suppress the set |
38 * 'typedef' command has new option "open" to suppress the set |
35 definition; |
39 definition; |
36 |
40 |
37 * Functions Min and Max on finite sets have been introduced. |
41 * functions Min and Max on finite sets have been introduced (theory |
38 (theory Finite_Set) |
42 Finite_Set); |
39 |
43 |
40 * attribute [symmetric] now works for relations as well; it turns |
44 * attribute [symmetric] now works for relations as well; it turns |
41 (x,y) : R^-1 into (y,x) : R, and vice versa; |
45 (x,y) : R^-1 into (y,x) : R, and vice versa; |
42 |
46 |
43 * arith(_tac) now produces a counter example if it cannot prove a theorem. |
47 * arith(_tac) now produces a counter example if it cannot prove a theorem. |