changeset 10793 | 4d6cf7702e3c |
parent 10770 | 4858ad0b8f38 |
child 10799 | ea69ee7e117b |
--- a/NEWS Fri Jan 05 18:16:01 2001 +0100 +++ b/NEWS Fri Jan 05 18:31:48 2001 +0100 @@ -1,4 +1,3 @@ - Isabelle NEWS -- history user-relevant changes ============================================== @@ -11,6 +10,9 @@ * HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp; +* HOL: infix "dvd" now has priority 50 rather than 70 + (because it is a relation) + * Isar: 'obtain' no longer declares "that" fact as simp/intro; * Isar/HOL: method 'induct' now handles non-atomic goals; as a