next up previous contents
Next: Printing a Proof Tree Up: Reference Material for Tutorial Previous: Tactics

Printing Transcripts

To print up a transcript file, you can use the ML function latexize_file to create a LATEXable version of it. latexize_file has ML type string -> string -> unit. The first argument should be the name of a transcript file. The second the name of the file you want the LATEXized version of the transcript written to. For example, if you have written a transcript to the file ~/tx1.prl, you might type:

ML top loop
 
M>latexize_file "~/tx1.prl" "~/tx1.tex" ;;
 
 


Dora Abdullah, 12/4/97