* 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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
