Dear Isabelle,
I have a theorem.

theorem t: "......"

To *state* my theorem is quite straightforward, but to *prove* it I require a whole bunch of other lemmas, definitions and datatypes. My theory file, therefore, looks like this:

definition x1: "......"
datatype x2 = ......
definition x3: "......"
lemma x4: "......"
datatype x5 = ......
lemma x6: "......"
theorem t: "......."
proof ......

Something about this strikes me as sub-optimal. The lemmas, definitions and datatypes x1...x6 are only required *within* this one particular proof. It seems like a violation of modularity for them to be globally-available outside of this proof. So I would prefer my theory file to look like this:

theorem t: "......."
proof
definition x1: "......"
datatype x2 = ......
definition x3: "......"
lemma x4: "......"
datatype x5 = ......
lemma x6: "......"
......
qed

I know I can already kind-of define lemmas within a proof (by writing "have x4: ...") and I know I can already kind-of make definitions within a proof (by writing "let ..." or "def ..."). But what would be quite nice would be to have the *full* expressivity that is available at the "top-level", also available within a proof, so that I can make proof-local datatypes, typedefs, and so on.
cheers,
john