equal
deleted
inserted
replaced
95 (only makes sense in practice, if outer syntax is delimited |
95 (only makes sense in practice, if outer syntax is delimited |
96 differently). |
96 differently). |
97 |
97 |
98 |
98 |
99 *** HOL *** |
99 *** HOL *** |
|
100 |
|
101 * Simplifier: Enhanced solver of preconditions of rewrite rules |
|
102 can now deal with conjunctions. |
|
103 For help with converting proofs, the old behaviour of the simplifier |
|
104 can be restored like this: declare/using [[simp_legacy_precond]] |
|
105 This configuration option will disappear again in the future. |
100 |
106 |
101 * HOL-Word: |
107 * HOL-Word: |
102 * Abandoned fact collection "word_arith_alts", which is a |
108 * Abandoned fact collection "word_arith_alts", which is a |
103 duplicate of "word_arith_wis". |
109 duplicate of "word_arith_wis". |
104 * Dropped first (duplicated) element in fact collections |
110 * Dropped first (duplicated) element in fact collections |