Commit 0bc081ae authored by MARCHE Claude's avatar MARCHE Claude

un 'ensures' bizarrement en trop

parent a0084b8f
(**
ensures {1 The VerifyThis competition at FM2012: Problem 2}
{1 The VerifyThis competition at FM2012: Problem 2}
see {h <a href="http://fm2012.verifythis.org/challenges">this web page</a>}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment