MoreDeclarationsShouldBeAllowedInMutualBlocks

I want all declarations to be allowed in mutual blocks, unless there is a good (documented) reason not to allow them. Arbitrary restrictions do not make the language easier to understand. Specifically, the following declarations would be nice:

• Postulates.
• Modules.