src/Doc/Isar_Ref/HOL_Specific.thy
changeset 81706 7beb0cf38292
parent 80914 d97fdabd9e2b
child 81989 96afb0707532
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -2314,7 +2314,7 @@
     ;
     @@{command (HOL) code_deps} (const_expr+)
     ;
-    @@{command (HOL) code_reserved} target (@{syntax string}+)
+    @@{command (HOL) code_reserved} ('(' target ')' (@{syntax string}+) + @'and')
     ;
     symbol_const: @'constant' const
     ;