equal
deleted
inserted
replaced
228 theorem (i.e. lhs and rhs exchanged) is added to the simpset. For "auto" |
228 theorem (i.e. lhs and rhs exchanged) is added to the simpset. For "auto" |
229 and friends the modifier is "simp flip:". |
229 and friends the modifier is "simp flip:". |
230 |
230 |
231 |
231 |
232 *** HOL *** |
232 *** HOL *** |
|
233 |
|
234 * Sledgehammer: bundled version of "vampire" (for non-commercial users) |
|
235 helps to avoid fragility of "remote_vampire" service. |
233 |
236 |
234 * Clarified relationship of characters, strings and code generation: |
237 * Clarified relationship of characters, strings and code generation: |
235 |
238 |
236 - Type "char" is now a proper datatype of 8-bit values. |
239 - Type "char" is now a proper datatype of 8-bit values. |
237 |
240 |