src/HOL/SPARK/Manual/Example_Verification.thy
changeset 59587 8ea7b22525cb
parent 58622 aa99568f56de
child 63167 0909deb8059b