This may not be directly relevant to your question but you could consider
developing your proofs interactively in an editor (Vim or Emacs) and saving
the scripts instead of using the HOL4 REPL directly (see the various proof
scripts in src/ and examples/).
I use the Vim bindings:
--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Hi,
there is also the GoalTree library. In contrast to the GoalStack one,
expanding a tactic gets the tactic twice. Once as a string and once as a
ML function. This allows the GoalTree to keep track of the proof
stucture and print the tactics used for the proof using THEN, THENL,
etc. at the
THEN applies the tactic to all subgoals, THEN1 applies it to the first one
(and expects it to be solved) -- Refer to the HOL reference for a full
explanation
So your final proof might look like
fs[]>>rw[]
(*Suppose we generated 5 subgoals*)
>- (*first subgoal tactic*)
( a >> b >> c)
>- (*
