I have a set of theorems, which state: let thm1 = A;; let thm2 = A <=> B;;
And I want a theorem that states B. I tried making B my goal, and using MESON_TAC[thm1,thm2] but MESON timed out. What’s the proper way to prove B? ------------------------------------------------------------------------------ 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
