You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
As per Hasan Amjad’s TPHOLs’05 paper. These could be used interactively at the level of calls to prove and store_thm, with worker thread(s) spawned to handle proofs in the background. I think the extra assumptions needed to make the theorem valid should be a transient constant defined to be equal to the desired goal. The VALID tactical could then ignore extra assumptions that looked like such constants so that previously proved theorems could be used in subsequent tactics.
The text was updated successfully, but these errors were encountered:
As per Hasan Amjad’s TPHOLs’05 paper. These could be used interactively at the level of calls to
prove
andstore_thm
, with worker thread(s) spawned to handle proofs in the background. I think the extra assumptions needed to make the theorem valid should be a transient constant defined to be equal to the desired goal. TheVALID
tactical could then ignore extra assumptions that looked like such constants so that previously proved theorems could be used in subsequent tactics.The text was updated successfully, but these errors were encountered: