src/HOL/SPARK/Manual/document/loop_invariant.ads
changeset 60299 5ae2a2e74c93
parent 45044 2fae15f8984d