Add support for exercises

[SReichelt]

There are many ways in which exercises could work. Some ideas:

• "Exercise" can be a theorem type like "proposition", "lemma", etc.
• Theorems marked this way should behave somewhat differently:
  • Existing proofs (if any) are hidden from the user, e.g. "Proof. Exercise."
  • Normal edit operations are disabled.
  • Instead, there is a large "Start" button next to the proof label, which switches to proof input.
  • Once the proof is finished, a "congratulations" message is displayed, with optional further information stored with the theorem.
  • There should probably be some notion of a "next exercise".
• Furthermore, it would be useful to have one or more separate libraries designed specifically for exercises, similarly to Kevin Buzzard's Natural number game for Lean.