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

Jon Lockhart
Proofpower mailing list

Reply via email to