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 ;