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

Makarius makarius at sketis.net
Wed Jun 24 21:46:04 CEST 2015

* 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
     show A by simp
     show A by simp

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".


More information about the isabelle-dev mailing list