Apparently Coq somewhat recently gained the ability to be explicit about proof structure: http://poleiro.info/posts/2013-06-27-structuring-proofs-with-bullets.html (Of course that comes naturally when using tacticals like THEN, THEN1, etc.)
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
