Date: Wednesday, 27 February 2019 at 15:23
To: hol-info
Subject: Re: [Hol-info] Working with assumptions
Hi Michael,
Thanks for your help! I wasn't subscribed to the mailing list so I only saw
your response in the mail archive. I have since properly signed up for the list.
I have a questi
Hi Michael,
Thanks for your help! I wasn't subscribed to the mailing list so I only saw
your response in the mail archive. I have since properly signed up for the
list.
I have a question on pattern matching on the assumptions: what is meant by
a pattern and where is it defined? Does `!x. P` match
Hi Haitao,
I’m glad you figured out sg and metis_tac as a solution to this, but of course,
you’re right that this can be tedious. One of the most precise way of attacking
this is to use a tactic like drule, and to select assumptions with the various
_assum combinators (first_assum, last_assum,
