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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to