Dave,

It's done using:

=GFT ProofPower output

"=GFT" stands for something like "General Formal Text". The text on the
GFT line is used for the label and the lines coming after a GFT directive are
just formatted like formal text in theLaTeX document, but not included by 
docsml.
I would typically copy text out of the journal window and paste it into the 
script
window while writing the document and processing the SML that produces
the output interactively.

Regards,

Rob.

> On 15 Feb 2019, at 18:17, David Topham <[email protected]> wrote:
> 
> I was reading an article by Rob Arthan about ProofPower Z and notice that the 
> document shows SML input followed by ProofPower output. I have not seen how 
> to automatically create that using xpp. e.g. I know that
> =SML
> produces the first label using doctex, but what produces the "ProofPower 
> output" label in the tex file?
> 
> So far, I have been using screenshot images of what I see in xpp and using 
> \includegraphics under =TEX
> -- 
> -Dave
> _______________________________________________
> Proofpower mailing list
> [email protected]
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com


_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to