# HG changeset patch
# User haftmann
# Date 1649496429 -7200
# Node ID 7b75a2c5b142f3cf407a6e0b1eecf08b25561773
# Parent  9c0300345e174ad085b0c8a5b60adfe9336e0f7a
more correct language

diff -r 9c0300345e17 -r 7b75a2c5b142 src/Doc/Isar_Ref/HOL_Specific.thy
--- 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.