On 08/23/2017 09:03 AM, michael.norr...@data61.csiro.au wrote:
You are being caught by the fact that match_mp_tac thm can throw an exception
before the tactic is ever applied to a goal. In particular, if the theorem
passed to match_mp_tac is not an implication an exception is thrown immediately.
You can fix this by handling that possible exception:
fun simple_apply thm = ACCEPT_TAC thm ORELSE (match_mp_tac thm handle HOL_ERR
_ => ALL_TAC)
Thank you for the fix. With this I could come up with a solution that I
find ok for the moment:
val my_match_mp_tac = (fn thm => (fn gs => match_mp_tac thm gs))
This allows to at least not have the HOL_ERR handling, but I guess it
depends what one finds nicer.
This arguably a poor design for match_mp_tac, and should perhaps be changed.
Looking at the definition of MATCH_MP_TAC, I found a pretty easy fix,
that should remove this behavior, thus I opened Pull Request #455
<https://github.com/HOL-Theorem-Prover/HOL/pull/455>.
Cheers,
Heiko
------------------------------------------------------------------------------
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
