`Statement` quotation filter syntax

[hrutvik]

It is not uncommon to have a theory file which proves a single, relatively clean theorem - but the purpose of the file is cluttered by various intermediate definition and lemmas. One possible solution is to declare top-level definitions and theorem statements at the top of a file so that they are easily identified.

Currently there is no clean way of doing this - something like the following is an approximation:

<definitions required for theorem statement>

val thm_statement = ``<desired theorem>``;

<all the intermediate definitions/lemmas>

Theorem thm:
  ^thm_statement
Proof
 ...
QED

I propose a quotation filter syntax:

<definitions required for theorem statement>

Statement thm_statement:
  <desired theorem>
End

<all the intermediate definitions/lemmas>

Proof of thm_statement[attributes]:
  ...
QED

Care would be needed to ensure that theorem statement bindings do not get overwritten, and that interaction is relatively straightforward.

As discussed on Slack and in PureCake meeting.