src/HOL/SPARK/Manual/document/loop_invariant.adb
changeset 69454 ef051edd4d10
parent 45044 2fae15f8984d