src/Doc/Isar_Ref/HOL_Specific.thy
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'