[isabelle-dev] Redundant equations in function declarations

Alexander Krauss krauss at in.tum.de
Thu Jun 7 21:47:18 CEST 2012

> 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.


More information about the isabelle-dev mailing list