Amjad style lazy theorems

[mn200]

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.