diff --git a/docs/users_guide/9.10.1-notes.rst b/docs/users_guide/9.10.1-notes.rst
index 38bbcae39f897342cda3cb68d3cff8a037ddec79..cb87ee167cc975b3701e55e65f56e38e806c40ef 100644
--- a/docs/users_guide/9.10.1-notes.rst
+++ b/docs/users_guide/9.10.1-notes.rst
@@ -124,6 +124,20 @@ Language
 
   The extension is enabled by default, establishing the usual behavior.
 
+- In accordance with GHC Proposal `#448 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0448-type-variable-scoping.rst>`_,
+  the :extension:`TypeAbstractions` extension has been extended to support
+  ``@``-binders in lambdas and function equations::
+
+    id :: forall a. a -> a
+    id @t x = x :: t
+    -- ^^ @-binder in a function equation
+
+    e = higherRank (\ @t -> ... )
+    --                ^^ @-binder in a lambda
+
+  This feature is an experimental alternative to :extension:`ScopedTypeVariables`,
+  see the :ref:`type-abstractions-in-functions` section.
+
 Compiler
 ~~~~~~~~
 
diff --git a/docs/users_guide/exts/type_abstractions.rst b/docs/users_guide/exts/type_abstractions.rst
index 1b55c2b60257c727d3e5937b87d72e8ed7247f8e..925048e62b56b7a5093b9c94b05d3b632bf8d70c 100644
--- a/docs/users_guide/exts/type_abstractions.rst
+++ b/docs/users_guide/exts/type_abstractions.rst
@@ -6,7 +6,7 @@ Type abstractions
 
     :since: 9.8.1
 
-    :status: Partially implemented
+    :status: Experimental
 
     Allow the use of type abstraction syntax.
 
@@ -22,6 +22,8 @@ and `#425 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/
 Type Abstractions in Patterns
 -----------------------------
 
+**Since:** GHC 9.2
+
 The type abstraction syntax can be used in patterns that match a data
 constructor. The syntax can't be used with record patterns or infix patterns.
 This is useful in particular to bind existential type variables associated with
@@ -99,6 +101,8 @@ matched, rather than ever referring to a variable from an outer scope. Type wild
 Type Abstractions in Functions
 ------------------------------
 
+**Since:** GHC 9.10
+
 Type abstraction syntax can be used in lambdas and function left-hand sides to
 bring into scope type variables associated with invisible ``forall``.
 For example::
@@ -200,6 +204,8 @@ At the moment, an ``@``-binder is valid only in a limited set of circumstances:
 Invisible Binders in Type Declarations
 --------------------------------------
 
+**Since:** GHC 9.8
+
 Syntax
 ~~~~~~