> I may as well be a bit more explicit. About seven Cambridge MPhil students were > given an assignment that included converting the following ML code into HOL and > proving theorems about it. [...] OK. See now e7e647949c95, as a reaction to this tragic story. Alex