equal
deleted
inserted
replaced
1 |
|
2 Isabelle NEWS -- history user-relevant changes |
1 Isabelle NEWS -- history user-relevant changes |
3 ============================================== |
2 ============================================== |
4 |
3 |
5 New in this Isabelle version |
4 New in this Isabelle version |
6 ---------------------------- |
5 ---------------------------- |
28 definition package, has lost an argument. To simplify its result, it |
27 definition package, has lost an argument. To simplify its result, it |
29 uses the default simpset instead of a supplied list of theorems. |
28 uses the default simpset instead of a supplied list of theorems. |
30 |
29 |
31 * HOL/List: the constructors of type list are now Nil and Cons; |
30 * HOL/List: the constructors of type list are now Nil and Cons; |
32 |
31 |
|
32 * Simplifier: the type of the infix ML functions |
|
33 setSSolver addSSolver setSolver addSolver |
|
34 is now simpset * solver -> simpset where `solver' is a new abstract type |
|
35 for packaging solvers. A solver is created via |
|
36 mk_solver: string -> (thm list -> int -> tactic) -> solver |
|
37 where the string argument is only a comment. |
33 |
38 |
34 *** Proof tools *** |
39 *** Proof tools *** |
35 |
40 |
36 * Provers/Arith/fast_lin_arith.ML contains a functor for creating a |
41 * Provers/Arith/fast_lin_arith.ML contains a functor for creating a |
37 decision procedure for linear arithmetic. Currently it is used for |
42 decision procedure for linear arithmetic. Currently it is used for |