pvs-realize.drv 186 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11

(*
prelude "% This file is generated by Why3's PVS driver"
prelude "% Beware! Only edit allowed sections below   "
*)

printer "pvs-realize"
filename "%t.pvs"

import "pvs-common.gen"