Milestone examples

• bakery.lean (depends on Bakery/DMC.lean)
• nsl-computational.lean (depends on Bakery/S4.lean)

Working examples

• qlock-compositional (depends on Bakery/DMC3.lean)
  • c.f., mono-vs-modu.lean (modular specification demo)