equal
deleted
inserted
replaced
36 * Provers/Arith/fast_lin_arith.ML contains a functor for creating a |
36 * Provers/Arith/fast_lin_arith.ML contains a functor for creating a |
37 decision procedure for linear arithmetic. Currently it is used for |
37 decision procedure for linear arithmetic. Currently it is used for |
38 types `nat' and `int' in HOL (see below) but can, should and will be |
38 types `nat' and `int' in HOL (see below) but can, should and will be |
39 instantiated for other types and logics as well. |
39 instantiated for other types and logics as well. |
40 |
40 |
|
41 * The simplifier now accepts rewrite rules with flexible heads, eg |
|
42 hom ?f ==> ?f(?x+?y) = ?f ?x + ?f ?y |
|
43 They are applied like any rule with a non-pattern lhs, i.e. by first-order |
|
44 matching. |
41 |
45 |
42 *** General *** |
46 *** General *** |
43 |
47 |
44 * new Isabelle/Isar subsystem provides an alternative to traditional |
48 * new Isabelle/Isar subsystem provides an alternative to traditional |
45 tactical theorem proving; together with the ProofGeneral/isar user |
49 tactical theorem proving; together with the ProofGeneral/isar user |