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
wishes,
Michael
From: Haitao Zhang
Date: Tuesday, 26 February 2019 at 09:12
To: hol-info
Subject: [Hol-info] Working with assumptions
Hi,
I just started HOL and am really enjoying it quite a bit. One difficulty I find
during interactive tactic proof sessions is to get hold of and manipulate
Hi,
I just started HOL and am really enjoying it quite a bit. One difficulty I
find during interactive tactic proof sessions is to get hold of and
manipulate assumptions. Right now I find myself using sg to write new
subgoals and then metis_tac[] to prove the baby steps that could be easily
proved
