[isabelle-dev] NEWS: nesting of Isar goal structure

[Makarius]

* Nesting of Isar goal structure has been clarified: the context after
the initial backwards refinement is retained for the whole proof, within
all its context sections (as indicated via 'next'). This is e.g.
relevant for 'using', 'including', 'supply':

   have "A ∧ A" if a: A for A
     supply [simp] = a
   proof
     show A by simp
   next
     show A by simp
   qed


This refers to Isabelle/2b8342b0d98c.  The block structure now conforms 
better to contemporay Isar, with its various ways to operate in the 
backwards refinement are, which is sometimes used for "proof scripting".


 	Makarius