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: https://github.com/HOL-Theorem-Prover/HOL/tree/master/tools/vim and others may be able to tell you more about the emacs ones. Usual development (for me in Vim): 1) State the goal in your proof script like: val foo = prove (``g``, 2) Highlight ``g`` and send it to the theorem prover as a goal (h-t , h-g) 3) Start writing and trying tactics (h-e sends the tactic to the prover, see the README for other things you could do) val foo = prove(``g``, fs[] >> rw[] >> blabla... (>> is THEN, >- is THEN1) 4) On a successful proof, just save whatever you wrote in the editor into a proof file: val foo = prove(``g``, fs[]>>rw[]>>blabla); This is off the top of my head, there might be a better guide for this somewhere. On Sun, Nov 15, 2015 at 5:39 PM, Ramana Kumar <[email protected]> wrote: > Use Tactical.THEN (or lcsymtacs.>>, which is the same). > > On 15 November 2015 at 09:03, shengyu shen <[email protected]> wrote: > >> Dear all : >> >> Supposing I have goal G and I prove it with lots of tactics like folowing >> : >> >> >> g `G`; >> e (t1); >> e (t2); >> e (t3); >> >> So after I finished proof, I need to use store_thm to manually collecting >> all t1,t2,t3... to save the proven theorem. >> >> Is there any way to automatically collect all these tactics? >> >> >> Shen >> >> >> ------------------------------------------------------------------------------ >> >> _______________________________________________ >> hol-info mailing list >> [email protected] >> https://lists.sourceforge.net/lists/listinfo/hol-info >> >> > > > ------------------------------------------------------------------------------ > > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info > >
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
