| changeset 81591 | d570d215e380 |
| parent 81514 | 98cb63b447c6 |
| child 81989 | 96afb0707532 |
--- a/src/Doc/Isar_Ref/Spec.thy Sat Dec 14 17:35:53 2024 +0100 +++ b/src/Doc/Isar_Ref/Spec.thy Sat Dec 14 21:47:20 2024 +0100 @@ -293,6 +293,7 @@ the polarity of certain declaration commands should be inverted, notably: \<^item> @{command syntax} versus @{command no_syntax} + \<^item> @{command translations} versus @{command no_translations} \<^item> @{command notation} versus @{command no_notation} \<^item> @{command type_notation} versus @{command no_type_notation}