Hi,
You can rewrite your goal with thm2 by using
e (SIMP_TAC [GSYM thm2]);
and then use
e (SIMP_TAC [thm1]);
On Wed, Jul 18, 2018 at 4:43 PM Dylan Melville <dylanmelvi...@gmail.com>
wrote:
> 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
>
--
Waqar Ahmad, Ph.D.
Post Doc at Hardware Verification Group (HVG)
Department of Electrical and Computer Engineering
Concordia University, QC, Canada
Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
------------------------------------------------------------------------------
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
