src/HOL/SPARK/Manual/document/complex_types_app.ads
author nipkow
Sat, 06 Apr 2013 18:42:55 +0200
changeset 51628 0a6d576da295
parent 45044 2fae15f8984d
permissions -rw-r--r--
tuned

with Complex_Types;
--# inherit Complex_Types;

package Complex_Types_App
is

   procedure Initialize (A : in out Complex_Types.Array_Type2);
   --# derives A from A;
   --# post Complex_Types.Initialized (A, 10);

end Complex_Types_App;