make WWW_Find work again, now that its ML modules reside within a theory context (cf. bf5b45870110) -- patch by Rafal Kolanski;
package body Loop_Invariant
is
procedure Proc1 (A : in Natural; B : in Word32; C : out Word32)
is
begin
C := 0;
for I in Natural range 1 .. A
--# assert Word32 (I - 1) * B = C;
loop
C := C + B;
end loop;
end Proc1;
procedure Proc2 (A : in Natural; B : in Word32; C : out Word32)
is
begin
C := 0;
for I in Natural range 1 .. A
--# assert Word32 (I - 1) * B = C;
loop
C := C + B;
--# assert Word32 (I) * B = C;
end loop;
end Proc2;
end Loop_Invariant;