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

Attachment: 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

Reply via email to