Dear Community, I was wondering if any of you knew of a command that could be used while writing your ProofPower proofs for you HOL or Zed specifications that would allow for the application of the apply_tactic or a command a predetermined number of times? In my specifications I am running across an instance where I need to repeat the same proof command for several goal statements in a row. For example I could have 3 or 4 goals that all require the command 'a (PC_T1 "z_lin_arith asm_prove_tac [])'. Rather than repeating this multiple times I would like to encapsulate the whole thing in a loop or a repeat function, similar to the use of REPEAT within a goal to apply the tactic multiple times. Does such a function exist within the ProofPower tool environment?
Regards, Jon Lockhart
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
