I wrote a “ssfrag” to simplify conjunctions and disjunctions in the aforementioned way plus normalization to right associativity, based on AC_Sort. It is in my repository of HOL4 developments <https://puszcza.gnu.org.ua/projects/hol-proofs>, file “marioxcc_lib.sml”.
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
