summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

NEWS

changeset 54893 | 4061ec8adb1c |

parent 54890 | cb892d835803 |

child 55001 | f26a7f06266d |

--- a/NEWS Wed Jan 01 01:05:48 2014 +0100 +++ b/NEWS Wed Jan 01 12:57:26 2014 +0100 @@ -33,10 +33,10 @@ *** HOL *** -* "declare [[code abort: …]]" replaces "code_abort …". -INCOMPATIBILITY. - -* "declare [[code drop: …]]" drops all code equations associated +* "declare [[code abort: ...]]" replaces "code_abort ...". +INCOMPATIBILITY. + +* "declare [[code drop: ...]]" drops all code equations associated with the given constants. * Abolished slightly odd global lattice interpretation for min/max. @@ -121,7 +121,7 @@ * When devising rule sets for number calculation, consider the following canonical cases: 0, 1, numeral _, - 1, - numeral _. * HOLogic.dest_number also recognizes numerals in non-canonical forms - like "numeral One", "- numeral One", "- 0" and even "- … - _". + like "numeral One", "- numeral One", "- 0" and even "- ... - _". * Syntax for negative numerals is mere input syntax. INCOMPATBILITY. @@ -155,7 +155,7 @@ Consider simplification with algebra_simps or field_simps. b) Lifting rules from addition to subtraction: -Try with "using <rule for addition> of [… "- _" …]" by simp". +Try with "using <rule for addition> of [... "- _" ...]" by simp". c) Simplification with "diff_def": just drop "diff_def". Consider simplification with algebra_simps or field_simps;