CVS difference for ai12s/ai12-0112-1.txt

Differences between 1.25 and version 1.26
Log of other versions for file ai12s/ai12-0112-1.txt

--- ai12s/ai12-0112-1.txt	2020/04/22 01:00:05	1.25
+++ ai12s/ai12-0112-1.txt	2020/05/29 02:18:13	1.26
@@ -2611,9 +2611,9 @@
 @xcode<   @b<procedure> Move (Target : @b<in out> Holder; Source : @b<in out> Holder);>
 @dby
 @xcode<   @b<procedure> Move (Target : @b<in out> Holder; Source : @b<in out> Holder)
-      @b<with> Pre  =@> ((@b<not> Tampering_With_The_Element_Prohibited (Target))
+      @b<with> Pre  =@> (@b<not> Tampering_With_The_Element_Prohibited (Target)
                        @b<or else raise> Program_Error) @b<and then>
-                   ((@b<not> Tampering_With_The_Element_Prohibited (Source))
+                   (@b<not> Tampering_With_The_Element_Prohibited (Source)
                        @b<or else raise> Program_Error),
            Post =@> (@b<if> Target /= Source @b<then>
                        Is_Empty (Source) @b<and then> (@b<not> Is_Empty (Target)));>
@@ -2625,9 +2625,9 @@
 @xcode<@b<procedure> Move (Target : @b<in out> Holder; Source : @b<in out> Holder);>
 @dby
 @xcode<@b<procedure> Move (Target : @b<in out> Holder; Source : @b<in out> Holder)
-   @b<with> Pre  =@> ((@b<not> Tampering_With_The_Element_Prohibited (Target))
+   @b<with> Pre  =@> (@b<not> Tampering_With_The_Element_Prohibited (Target)
                     @b<or else raise> Program_Error) @b<and then>
-                ((@b<not> Tampering_With_The_Element_Prohibited (Source))
+                (@b<not> Tampering_With_The_Element_Prohibited (Source)
                     @b<or else raise> Program_Error),
         Post =@> (@b<if> Target /= Source @b<then>
                     Is_Empty (Source) @b<and then> (@b<not> Is_Empty (Target)));>

Questions? Ask the ACAA Technical Agent