--- a/src/Doc/Isar_Ref/HOL_Specific.thy Thu Mar 28 13:06:32 2019 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Thu Mar 28 13:20:57 2019 +0100
@@ -2345,9 +2345,12 @@
('(' target ')' '-' ? + @'and')
;
printing_module: symbol_module ('\<rightharpoonup>' | '=>') \<newline>
- ('(' target ')' \<newline>
- (@{syntax string}
- (@'for' ((symbol_const | symbol_type_constructor | symbol_class | symbol_class_relation | symbol_class_instance)+))?)? + @'and')
+ ('(' target ')' (@{syntax string} for_symbol?)? + @'and')
+ ;
+ for_symbol:
+ @'for'
+ ((symbol_const | symbol_typeconstructor |
+ symbol_class | symbol_class_relation | symbol_class_instance)+)
;
@@{command (HOL) code_printing} ((printing_const | printing_type_constructor
| printing_class | printing_class_relation | printing_class_instance