--- a/src/Doc/Isar_Ref/HOL_Specific.thy Fri Apr 08 17:17:21 2022 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Sat Apr 09 11:27:09 2022 +0200
@@ -2436,9 +2436,8 @@
Variants \<open>code drop:\<close> and \<open>code abort:\<close> take a list of constants as arguments
and drop all code equations declared for them. In the case of \<open>abort\<close>,
- these constants then do not require to a specification by means of
- code equations; if needed these are implemented by program abort (exception)
- instead.
+ these constants if needed are implemented by program abort
+ (exception).
Packages declaring code equations usually provide a reasonable default
setup.