Install monad syntax by default

[mn200]

For backwards compatibility, there could be a theory-level command that turned this back off again, but I think monadsyntax should be available by default, perhaps binding to the option monad. That second choice could be extended or overridden with other monads too.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.