How to make the assumption of the second case of an Isabelle/Isar proof by cases explicit right in place?

Question

I have an Isabelle proof structured as follows:

proof (cases "n = 0")
  case True
  (* lots of stuff here *)
  show ?thesis sorry
next
  case False
  (* lots of stuff here too *)
  show ?thesis sorry
qed

The first case is actually several pages long, so when reading the second case it's no longer clear to a casual reader, not even to myself, what the False refers to. (Well, it actually is, but not from reading, only in an interactive environment: If, e.g., in Isabelle/jEdit, you place the cursor after case False, you'll see n ≠ 0 under "this" in the Output panel.)

So is there a syntax that allows for making the assumption of the "False" case explicit, so that the reader neither has to interact with the IDE, nor to scroll up to the proof keyword, but can see the assumption right in place?

Answer 1

In this case the proof becomes more readable by stating the assumption of each case explicitly:

proof cases
  assume "n = 0"
  show ?thesis sorry
next
  assume "n ≠ 0"
  show ?thesis sorry
qed