HOL-SPARK-Manual

Simple_Greatest_Common_Divisor

Example_Verification

Proc1

Proc2

VC_Principles

Reference

Complex_Types