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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
