changeset 82379 | 3f875966c3e1 |
parent 82378 | 23df00d48d6f |
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Sun Mar 30 11:21:34 2025 +0200 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Sun Mar 30 13:50:06 2025 +0200 @@ -2312,7 +2312,8 @@ ('(' target ')' '-' ? + @'and') ; printing_module: symbol_module ('\<rightharpoonup>' | '=>') \<newline> - ('(' target ')' (target_syntax for_symbol?)? + @'and') + ('(' target ')' \<newline> + ((target_syntax | @'file' path) for_symbol?)? + @'and') ; for_symbol: @'for'