Menu
▾
▴
#24 VCG PO insert - include zproof
When inserting VCG proof obligations via double-click, it would be good to include the zproof environment as well immediately after the definition (or have an option for that). Note that this may be not a preferred option if proofs are in a separate file than the theorem definitions.
