Just adding a success note: I finished HOL Light versions of the Benes-network theorems---
https://cr.yp.to/papers.html#controlbits https://cr.yp.to/2020/controlbits-20200923.ml ---and I think that asking my readers to check the HOL Light versions of the definitions and main theorems against the intended results is much less of an imposition than asking them to check my proofs in English. I noticed that I'm finishing proofs with MESON_TAC much more often than *.ml and Library/*.ml are, which could relate to my taking smaller steps from one theorem to the next, or to my not knowing many alternative ways to finish HOL Light proofs. :-) ---Dan
signature.asc
Description: PGP signature
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
