diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
index 6124b11a42c..f9ee0efba94 100644
--- a/RELEASE_NOTES.md
+++ b/RELEASE_NOTES.md
@@ -2,6 +2,30 @@
 
 See [docs/dev/news/](docs/dev/news/).
 
+# 4.6.0
+
+## New features
+
+- Add a check to `dafny run` that notifies the user when a value that was parsed as a user program argument, and which occurs before a `--` token, starts with `--`, since this indicates they probably mistyped a Dafny option name. (https://github.com/dafny-lang/dafny/pull/5097)
+
+- Add an option --progress that can be used to track the progress of verification. (https://github.com/dafny-lang/dafny/pull/5150)
+
+- Add the attribute `{:isolate_assertions}`, which does the same as `{:vcs_split_on_every_assert}`. Deprecated `{:vcs_split_on_every_assert}` (https://github.com/dafny-lang/dafny/pull/5247)
+
+## Bug fixes
+
+- (soundness issue) Twostate predicate now check if their not new arguments are allocated in the previous heap (https://github.com/dafny-lang/dafny/pull/4844)
+
+- Add uniform checking of type characteristics in refinement modules (https://github.com/dafny-lang/dafny/pull/5146)
+
+- Fixed links associated with the standard libraries. (https://github.com/dafny-lang/dafny/pull/5176)
+
+- fix: Disable the "erase datatype wrappers" optimization if the datatype implements any traits.
+  feat: Allow the "erase datatype wrappers" optimization if the only fields in the datatype are ghost fields.
+  (https://github.com/dafny-lang/dafny/pull/5234)
+
+- Fix the default string value emitted for JavaScript (https://github.com/dafny-lang/dafny/pull/5239)
+
 # 4.5.0
 
 ## New features
diff --git a/docs/dev/news/4844.fix b/docs/dev/news/4844.fix
deleted file mode 100644
index 29dc060bae6..00000000000
--- a/docs/dev/news/4844.fix
+++ /dev/null
@@ -1 +0,0 @@
-(soundness issue) Twostate predicate now check if their not new arguments are allocated in the previous heap
\ No newline at end of file
diff --git a/docs/dev/news/5097.feat b/docs/dev/news/5097.feat
deleted file mode 100644
index b275d72aea1..00000000000
--- a/docs/dev/news/5097.feat
+++ /dev/null
@@ -1 +0,0 @@
-Add a check to `dafny run` that notifies the user when a value that was parsed as a user program argument, and which occurs before a `--` token, starts with `--`, since this indicates they probably mistyped a Dafny option name.
\ No newline at end of file
diff --git a/docs/dev/news/5146.fix b/docs/dev/news/5146.fix
deleted file mode 100644
index e3279703489..00000000000
--- a/docs/dev/news/5146.fix
+++ /dev/null
@@ -1 +0,0 @@
-Add uniform checking of type characteristics in refinement modules
diff --git a/docs/dev/news/5150.feat b/docs/dev/news/5150.feat
deleted file mode 100644
index e377e69fa5e..00000000000
--- a/docs/dev/news/5150.feat
+++ /dev/null
@@ -1 +0,0 @@
-Add an option --progress that can be used to track the progress of verification.
\ No newline at end of file
diff --git a/docs/dev/news/5176.fix b/docs/dev/news/5176.fix
deleted file mode 100644
index 9c980829d02..00000000000
--- a/docs/dev/news/5176.fix
+++ /dev/null
@@ -1 +0,0 @@
-Fixed links associated with the standard libraries.
\ No newline at end of file
diff --git a/docs/dev/news/5234.fix b/docs/dev/news/5234.fix
deleted file mode 100644
index 826c4a015ef..00000000000
--- a/docs/dev/news/5234.fix
+++ /dev/null
@@ -1,2 +0,0 @@
-fix: Disable the "erase datatype wrappers" optimization if the datatype implements any traits.
-feat: Allow the "erase datatype wrappers" optimization if the only fields in the datatype are ghost fields.
diff --git a/docs/dev/news/5239.fix b/docs/dev/news/5239.fix
deleted file mode 100644
index 901cf9369ba..00000000000
--- a/docs/dev/news/5239.fix
+++ /dev/null
@@ -1 +0,0 @@
-Fix the default string value emitted for JavaScript