author | haftmann |
Fri, 20 Jun 2008 21:01:17 +0200 | |
changeset 27305 | 2dbdfa495982 |
parent 27304 | 720c8115d723 |
child 27306 | 0609faccb903 |
--- a/NEWS Fri Jun 20 21:00:28 2008 +0200 +++ b/NEWS Fri Jun 20 21:01:17 2008 +0200 @@ -45,9 +45,6 @@ Suc_Suc_eq ~> nat.inject Suc_not_Zero Zero_not_Suc ~> nat.distinct -* 'Least' operator now restricted to class 'order' (and subclasses). -INCOMPATIBILITY. - * Library/Nat_Infinity: added addition, numeral syntax and more instantiations for algebraic structures. Removed some duplicate theorems. Changes in simp rules. INCOMPATIBILITY.