diff --git a/releases/v4.16.0.md b/releases/v4.16.0.md index a027cac4a25a..fd92fc998e4b 100644 --- a/releases/v4.16.0.md +++ b/releases/v4.16.0.md @@ -3,6 +3,7 @@ v4.16.0 ## Highlights ### Unique `sorry`s + [#5757](https://github.com/leanprover/lean4/pull/5757) makes it harder to create "fake" theorems about definitions that are stubbed-out with `sorry` by ensuring that each `sorry` is not definitionally equal to any other. For example, this now fails: