src/HOL/SPARK/Manual/document/loop_invariant.ads
changeset 78947 2a27d2c8eae8
parent 45044 2fae15f8984d