[isabelle-dev] Referring to unfolded chained facts

[Alexander Krauss]

> Here's an example. After "unfolding null_def", the user invoked Sledgehammer and asked for an Isar proof. The "proof - ... qed" block after that is generated by Sledgehammer:
>
>      lemma "null xs ==>  tl xs = xs"
>      proof -
>        assume nx: "null xs"
>        show "tl xs = xs"
>        using `null xs`
>        unfolding null_def
>        proof -
>          have "tl xs = []" by (metis `xs = []` tl.simps(1))
>          thus "tl xs = xs" by (metis `xs = []`)
>        qed

What about just generating

   assume "xs = []"

after "proof -" to properly introduce the unfolded proposition in the 
text. If you give it a name, it'll also be less verbose than the current 
version, since you don't have to repeat the proposition...

Alex