Phil,
Thank you very much for the quick response. The information you provided
was highly insightful and I will be sure to use the strategies you have
described in my current and future proofs.
You also provided me a solution with the last option you gave, as applying
the second to last tactic in
Hi Jon,
To keep proof scripts maintainable, I always strictly adhere to a format
where an SML comment is inserted each time the name of the goal changes.
For example:
val some_thm = (
push_goal ([], ...);
a (REPEAT z_strip_tac);
(* *** Goal "1" *** *)
a (...);
...
(* *** Goal "1.1" *** *)
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
